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,