# HG changeset patch
# User wenzelm
# Date 1459621431 -7200
# Node ID 744bfd770123199964a09afc9c9db83ece8edc50
# Parent  19387866eace3e65bceeeda1eece3ba2ac60e0e8
clarified modules;

diff -r 19387866eace -r 744bfd770123 src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 17:11:27 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 20:23:51 2016 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/ML/ml_compiler0.ML
+    Author:     Makarius
 
-Runtime compilation and evaluation (bootstrap version of
-Pure/ML/ml_compiler.ML).
+Runtime compilation and evaluation for bootstrap.
+Initial ML use operations.
 *)
 
 signature ML_COMPILER0 =
@@ -12,6 +13,7 @@
     here: int -> string -> string,
     print: string -> unit,
     error: string -> unit}
+  val make_context: ML_Name_Space.T -> context
   val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit
   val use_file: context -> {debug: bool, verbose: bool} -> string -> unit
   val debug_option: bool option -> bool
@@ -22,6 +24,16 @@
 structure ML_Compiler0: ML_COMPILER0 =
 struct
 
+(* global options *)
+
+val _ = PolyML.Compiler.reportUnreferencedIds := true;
+val _ = PolyML.Compiler.reportExhaustiveHandlers := true;
+val _ = PolyML.Compiler.printInAlphabeticalOrder := false;
+val _ = PolyML.Compiler.maxInlineSize := 80;
+
+
+(* context *)
+
 type context =
  {name_space: ML_Name_Space.T,
   print_depth: int option,
@@ -29,6 +41,18 @@
   print: string -> unit,
   error: string -> unit};
 
+fun make_context name_space : context =
+ {name_space = name_space,
+  print_depth = NONE,
+  here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
+  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
+  error = fn s => error s};
+
+
+(* use operations *)
+
+local
+
 fun drop_newline s =
   if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
   else s;
@@ -47,6 +71,8 @@
       | input _ [] res = rev res;
   in String.concat (input start_line (String.explode txt) []) end;
 
+in
+
 fun use_text ({name_space, print_depth, here, print, error, ...}: context)
     {line, file, verbose, debug} text =
   let
@@ -86,30 +112,28 @@
           error (output ()); Exn.reraise exn);
   in if verbose then print (output ()) else () end;
 
+end;
+
 fun use_file context {verbose, debug} file =
   let
     val instream = TextIO.openIn file;
     val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
 
+fun use_operations (use_ : bool option -> string -> unit) =
+  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
+
 
 fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
   | debug_option (SOME debug) = debug;
 
-fun use_operations (use_ : bool option -> string -> unit) =
-  {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)};
+end;
 
-end;
+
+(* initial use operations *)
 
 val {use, use_debug, use_no_debug} =
-  let
-    val context: ML_Compiler0.context =
-     {name_space = ML_Name_Space.global,
-      print_depth = NONE,
-      here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
-      print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
-      error = fn s => error s};
-  in
+  let val context = ML_Compiler0.make_context ML_Name_Space.global in
     ML_Compiler0.use_operations (fn opt_debug => fn file =>
       ML_Compiler0.use_file context
         {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
diff -r 19387866eace -r 744bfd770123 src/Pure/ML/ml_compiler1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler1.ML	Sat Apr 02 20:23:51 2016 +0200
@@ -0,0 +1,22 @@
+(*  Title:      Pure/ML/ml_compiler1.ML
+    Author:     Makarius
+
+Refined ML use operations for bootstrap.
+*)
+
+val {use, use_debug, use_no_debug} =
+  let
+    val context: ML_Compiler0.context =
+     {name_space = ML_Name_Space.global,
+      print_depth = NONE,
+      here = Position.here oo Position.line_file,
+      print = writeln,
+      error = error};
+  in
+    ML_Compiler0.use_operations (fn opt_debug => fn file =>
+      Position.setmp_thread_data (Position.file_only file)
+        (fn () =>
+          ML_Compiler0.use_file context
+            {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
+          handle ERROR msg => (writeln msg; error "ML error")) ())
+  end;
diff -r 19387866eace -r 744bfd770123 src/Pure/ML/ml_compiler2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler2.ML	Sat Apr 02 20:23:51 2016 +0200
@@ -0,0 +1,12 @@
+(*  Title:      Pure/ML/ml_compiler2.ML
+    Author:     Makarius
+
+Isabelle/ML use operations.
+*)
+
+val {use, use_debug, use_no_debug} =
+  ML_Compiler0.use_operations (fn opt_debug => fn file =>
+    let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
+      ML_Context.eval_file flags (Path.explode file)
+        handle ERROR msg => (writeln msg; error "ML error")
+    end);
diff -r 19387866eace -r 744bfd770123 src/Pure/ROOT
--- a/src/Pure/ROOT	Sat Apr 02 17:11:27 2016 +0200
+++ b/src/Pure/ROOT	Sat Apr 02 20:23:51 2016 +0200
@@ -101,6 +101,8 @@
     "ML/ml_antiquotation.ML"
     "ML/ml_compiler.ML"
     "ML/ml_compiler0.ML"
+    "ML/ml_compiler1.ML"
+    "ML/ml_compiler2.ML"
     "ML/ml_context.ML"
     "ML/ml_debugger.ML"
     "ML/ml_env.ML"
diff -r 19387866eace -r 744bfd770123 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Apr 02 17:11:27 2016 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 02 20:23:51 2016 +0200
@@ -63,11 +63,6 @@
 
 use "ML/ml_compiler0.ML";
 
-PolyML.Compiler.reportUnreferencedIds := true;
-PolyML.Compiler.reportExhaustiveHandlers := true;
-PolyML.Compiler.printInAlphabeticalOrder := false;
-PolyML.Compiler.maxInlineSize := 80;
-
 
 (* ML debugger *)
 
@@ -100,24 +95,7 @@
 use "General/input.ML";
 use "General/antiquote.ML";
 use "ML/ml_lex.ML";
-
-val {use, use_debug, use_no_debug} =
-  let
-    val context: ML_Compiler0.context =
-     {name_space = ML_Name_Space.global,
-      print_depth = NONE,
-      here = Position.here oo Position.line_file,
-      print = writeln,
-      error = error};
-  in
-    ML_Compiler0.use_operations (fn opt_debug => fn file =>
-      Position.setmp_thread_data (Position.file_only file)
-        (fn () =>
-          ML_Compiler0.use_file context
-            {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
-          handle ERROR msg => (writeln msg; error "ML error")) ())
-  end;
-
+use "ML/ml_compiler1.ML";
 
 
 (** bootstrap phase 2: towards ML within Isar context *)
@@ -287,13 +265,7 @@
 (*ML with context and antiquotations*)
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
-
-val {use, use_debug, use_no_debug} =
-  ML_Compiler0.use_operations (fn opt_debug => fn file =>
-    let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
-      ML_Context.eval_file flags (Path.explode file)
-        handle ERROR msg => (writeln msg; error "ML error")
-    end);
+use "ML/ml_compiler2.ML";