Mercurial > urweb
comparison src/compiler.sml @ 1637:e374b6b8ab38
Allow .urp libraries to set prefix
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 17 Dec 2011 13:10:23 -0500 |
parents | 438561303d02 |
children | 8de2ea0a0701 |
comparison
equal
deleted
inserted
replaced
1636:2b312f6d4007 | 1637:e374b6b8ab38 |
---|---|
498 readSources acc | 498 readSources acc |
499 end | 499 end |
500 | OnlyComment => readSources acc | 500 | OnlyComment => readSources acc |
501 | EndOfFile => rev acc | 501 | EndOfFile => rev acc |
502 | 502 |
503 val prefix = ref (case Settings.getUrlPrefix () of "/" => NONE | s => SOME s) | 503 val prefix = ref (case Settings.getUrlPrefixFull () of "/" => NONE | s => SOME s) |
504 val database = ref (Settings.getDbstring ()) | 504 val database = ref (Settings.getDbstring ()) |
505 val exe = ref (Settings.getExe ()) | 505 val exe = ref (Settings.getExe ()) |
506 val sql = ref (Settings.getSql ()) | 506 val sql = ref (Settings.getSql ()) |
507 val debug = ref (Settings.getDebug ()) | 507 val debug = ref (Settings.getDebug ()) |
508 val profile = ref false | 508 val profile = ref false |
578 ErrorMsg.error ("Multiple " | 578 ErrorMsg.error ("Multiple " |
579 ^ desc ^ " values that don't agree"); | 579 ^ desc ^ " values that don't agree"); |
580 x)) | 580 x)) |
581 | 581 |
582 fun merge (old : job, new : job) = { | 582 fun merge (old : job, new : job) = { |
583 prefix = #prefix old, | 583 prefix = case #prefix old of |
584 "/" => #prefix new | |
585 | pold => case #prefix new of | |
586 "/" => pold | |
587 | pnew => (if pold = pnew then | |
588 () | |
589 else | |
590 ErrorMsg.error ("Multiple prefix values that don't agree: " | |
591 ^ pold ^ ", " ^ pnew); | |
592 pold), | |
584 database = mergeO (fn (old, _) => old) (#database old, #database new), | 593 database = mergeO (fn (old, _) => old) (#database old, #database new), |
585 exe = #exe old, | 594 exe = #exe old, |
586 sql = #sql old, | 595 sql = #sql old, |
587 debug = #debug old orelse #debug new, | 596 debug = #debug old orelse #debug new, |
588 profile = #profile old orelse #profile new, | 597 profile = #profile old orelse #profile new, |