Alternate job-parsing interface, to avoid merging library directives

2 files changed, 37 insertions, 20 deletions

diff --git a/src/compiler.sig b/src/compiler.sig
index 2b08bff4..e34b771e 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2009, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -73,6 +73,7 @@ signature COMPILER = sig
     val parseUr : (string, Source.file) phase
     val parseUrs : (string, Source.sgn_item list) phase
     val parseUrp : (string, job) phase
+    val parseUrp' : (string, {Job : job, Libs : string list}) phase
 
     val parse : (job, Source.file) phase
     val elaborate : (Source.file, Elab.file) phase
@@ -104,6 +105,7 @@ signature COMPILER = sig
     val sqlify : (Mono.file, Cjr.file) phase
 
     val toParseJob : (string, job) transform
+    val toParseJob' : (string, {Job : job, Libs : string list}) transform
     val toParse : (string, Source.file) transform
     val toElaborate : (string, Elab.file) transform
     val toUnnest : (string, Elab.file) transform
diff --git a/src/compiler.sml b/src/compiler.sml
index baf8ddac..95ad80ad 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -104,20 +104,6 @@ fun transform (ph : ('src, 'dst) phase) name = {
               end
 }
 
-fun op o (tr2 : ('b, 'c) transform, tr1 : ('a, 'b) transform) = {
-    func = fn input => case #func tr1 input of
-                           NONE => NONE
-                         | SOME v => #func tr2 v,
-    print = #print tr2,
-    time = fn (input, pmap) => let
-                  val (ro, pmap) = #time tr1 (input, pmap)
-              in
-                  case ro of
-                      NONE => (NONE, pmap)
-                    | SOME v => #time tr2 (v, pmap)
-              end
-}
-
 fun check (tr : ('src, 'dst) transform) x = (ErrorMsg.resetErrors ();
                                              ignore (#func tr x))
 
@@ -284,9 +270,10 @@ structure M = BinaryMapFn(struct
                           val compare = String.compare
                           end)
 
-fun parseUrp' fname =
+fun parseUrp' accLibs fname =
     let
         val pathmap = ref (M.insert (M.empty, "", Config.libUr))
+        val bigLibs = ref []
 
         fun pu filename =
             let
@@ -431,7 +418,10 @@ fun parseUrp' fname =
                             dbms = mergeO #2 (#dbms old, #dbms new)
                         }
                     in
-                        foldr (fn (job', job) => merge (job, job')) job (!libs)
+                        if accLibs then
+                            foldr (fn (job', job) => merge (job, job')) job (!libs)
+                        else
+                            job
                     end
 
                 fun parsePkind s =
@@ -568,7 +558,10 @@ fun parseUrp' fname =
                                          fkind := {action = Settings.Deny, kind = kind, pattern = pattern} :: !fkind
                                      end
                                    | _ => ErrorMsg.error "Bad 'deny' syntax")
-                              | "library" => libs := pu (relify arg) :: !libs
+                              | "library" => if accLibs then
+                                                 libs := pu (relify arg) :: !libs
+                                             else
+                                                 bigLibs := relify arg :: !bigLibs
                               | "path" =>
                                 (case String.fields (fn ch => ch = #"=") arg of
                                      [n, v] => pathmap := M.insert (!pathmap, n, v)
@@ -597,15 +590,37 @@ fun parseUrp' fname =
                 job
             end
     in
-        pu fname
+        {Job = pu fname, Libs = !bigLibs}
     end
 
+fun p_job' {Job = j, Libs = _ : string list} = p_job j
+
 val parseUrp = {
-    func = parseUrp',
+    func = #Job o parseUrp' false,
     print = p_job
 }
 
+val parseUrp' = {
+    func = parseUrp' true,
+    print = p_job'
+}
+
 val toParseJob = transform parseUrp "parseJob"
+val toParseJob' = transform parseUrp' "parseJob'"
+
+fun op o (tr2 : ('b, 'c) transform, tr1 : ('a, 'b) transform) = {
+    func = fn input => case #func tr1 input of
+                           NONE => NONE
+                         | SOME v => #func tr2 v,
+    print = #print tr2,
+    time = fn (input, pmap) => let
+                  val (ro, pmap) = #time tr1 (input, pmap)
+              in
+                  case ro of
+                      NONE => (NONE, pmap)
+                    | SOME v => #time tr2 (v, pmap)
+              end
+}
 
 fun capitalize "" = ""
   | capitalize s = str (Char.toUpper (String.sub (s, 0))) ^ String.extract (s, 1, NONE)