--- 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
--- /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;
--- /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);
--- 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"
--- 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";