comparison src/compiler.sml @ 1336:7eefe077075a

Fix merging of prefix settings
author Adam Chlipala <adam@chlipala.net>
date Sun, 12 Dec 2010 10:57:41 -0500
parents 79557535b843
children 8c1996489265
comparison
equal deleted inserted replaced
1335:79557535b843 1336:7eefe077075a
615 (("", ""), ""))) 615 (("", ""), "")))
616 | _ => (ErrorMsg.error (cmd ^ " argument not of the form Module.func=func'"); 616 | _ => (ErrorMsg.error (cmd ^ " argument not of the form Module.func=func'");
617 (("", ""), "")) 617 (("", ""), ""))
618 in 618 in
619 case cmd of 619 case cmd of
620 "prefix" => 620 "prefix" => prefix := SOME arg
621 (case !prefix of
622 NONE => ()
623 | SOME _ => ErrorMsg.error "Duplicate 'prefix' directive";
624 prefix := SOME arg)
625 | "database" => 621 | "database" =>
626 (case !database of 622 (case !database of
627 NONE => database := SOME arg 623 NONE => database := SOME arg
628 | SOME _ => ()) 624 | SOME _ => ())
629 | "dbms" => 625 | "dbms" =>