# HG changeset patch # User wenzelm # Date 1456866696 -3600 # Node ID b90109b2487c897668f07aeb22c5f11f7f1e8ebb # Parent dd154240a53cea4192b227e1d52ce7770a7c26df clarified modules; diff -r dd154240a53c -r b90109b2487c src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Tue Mar 01 21:10:29 2016 +0100 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML Tue Mar 01 22:11:36 2016 +0100 @@ -184,7 +184,7 @@ in compiled_rewriter := NONE; - use_text ML_Env.local_context + ML_Compiler0.use_text ML_Env.local_context {line = 1, file = "", verbose = false, debug = false} (!buffer); case !compiled_rewriter of NONE => raise (Compile "cannot communicate with compiled function") diff -r dd154240a53c -r b90109b2487c src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Tue Mar 01 21:10:29 2016 +0100 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML Tue Mar 01 22:11:36 2016 +0100 @@ -486,7 +486,8 @@ fun writeTextFile name s = File.write (Path.explode name) s fun use_source src = - use_text ML_Env.local_context {line = 1, file = "", verbose = false, debug = false} src + ML_Compiler0.use_text ML_Env.local_context + {line = 1, file = "", verbose = false, debug = false} src fun compile rules = let diff -r dd154240a53c -r b90109b2487c src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Mar 01 21:10:29 2016 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Mar 01 22:11:36 2016 +0100 @@ -206,7 +206,7 @@ fun exec verbose code = ML_Context.exec (fn () => - use_text ML_Env.local_context + ML_Compiler0.use_text ML_Env.local_context {line = 0, file = "generated code", verbose = verbose, debug = false} code) fun with_overlord_dir name f = diff -r dd154240a53c -r b90109b2487c src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Tue Mar 01 21:10:29 2016 +0100 +++ b/src/Pure/ML/ml_env.ML Tue Mar 01 22:11:36 2016 +0100 @@ -14,7 +14,7 @@ val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T - val local_context: use_context + val local_context: ML_Compiler0.context val local_name_space: ML_Name_Space.T val check_functor: string -> unit end @@ -162,7 +162,7 @@ allFunct = all #6 #allFunct} end; -val local_context: use_context = +val local_context: ML_Compiler0.context = {name_space = name_space {SML = false, exchange = false}, here = Position.here oo Position.line_file, print = writeln, diff -r dd154240a53c -r b90109b2487c src/Pure/RAW/ROOT_polyml.ML --- a/src/Pure/RAW/ROOT_polyml.ML Tue Mar 01 21:10:29 2016 +0100 +++ b/src/Pure/RAW/ROOT_polyml.ML Tue Mar 01 22:11:36 2016 +0100 @@ -167,7 +167,7 @@ then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else (); use "RAW/ml_positions.ML"; -use "RAW/compiler_polyml.ML"; +use "RAW/ml_compiler0.ML"; PolyML.Compiler.reportUnreferencedIds := true; PolyML.Compiler.printInAlphabeticalOrder := false; diff -r dd154240a53c -r b90109b2487c src/Pure/RAW/compiler_polyml.ML --- a/src/Pure/RAW/compiler_polyml.ML Tue Mar 01 21:10:29 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,84 +0,0 @@ -(* Title: Pure/RAW/compiler_polyml.ML - -Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML). -*) - -type use_context = - {name_space: ML_Name_Space.T, - here: int -> string -> string, - print: string -> unit, - error: string -> unit}; - -local - -val boot_context: use_context = - {name_space = ML_Name_Space.global, - 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}; - -fun drop_newline s = - if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) - else s; - -in - -fun use_text ({name_space, here, print, error, ...}: use_context) - {line, file, verbose, debug} text = - let - val _ = Secure.deny_ml (); - - val current_line = Unsynchronized.ref line; - val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text)); - val out_buffer = Unsynchronized.ref ([]: string list); - fun output () = drop_newline (implode (rev (! out_buffer))); - - fun get () = - (case ! in_buffer of - [] => NONE - | c :: cs => - (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); - fun put s = out_buffer := s :: ! out_buffer; - fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} = - (put (if hard then "Error: " else "Warning: "); - PolyML.prettyPrint (put, 76) msg1; - (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); - put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n")); - - val parameters = - [PolyML.Compiler.CPOutStream put, - PolyML.Compiler.CPNameSpace name_space, - PolyML.Compiler.CPErrorMessageProc put_message, - PolyML.Compiler.CPLineNo (fn () => ! current_line), - PolyML.Compiler.CPFileName file, - PolyML.Compiler.CPPrintInAlphabeticalOrder false] @ - ML_Compiler_Parameters.debug debug; - val _ = - (while not (List.null (! in_buffer)) do - PolyML.compiler (get, parameters) ()) - handle exn => - if Exn.is_interrupt exn then reraise exn - else - (put ("Exception- " ^ General.exnMessage exn ^ " raised"); - error (output ()); reraise exn); - in if verbose then print (output ()) else () 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_debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true" - | use_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)}; - -val {use, use_debug, use_no_debug} = - use_operations (fn opt_debug => fn file => - use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file - handle ERROR msg => (#print boot_context msg; raise error "ML error")); - -end; diff -r dd154240a53c -r b90109b2487c src/Pure/RAW/ml_compiler0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/RAW/ml_compiler0.ML Tue Mar 01 22:11:36 2016 +0100 @@ -0,0 +1,100 @@ +(* Title: Pure/RAW/ml_compiler0.ML + +Runtime compilation and evaluation (bootstrap version of +Pure/ML/ml_compiler.ML). +*) + +signature ML_COMPILER0 = +sig + type context = + {name_space: ML_Name_Space.T, + here: int -> string -> string, + print: string -> unit, + error: string -> unit} + 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 + val use_operations: (bool option -> string -> unit) -> + {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit} +end; + +structure ML_Compiler0: ML_COMPILER0 = +struct + +type context = + {name_space: ML_Name_Space.T, + here: int -> string -> string, + print: string -> unit, + error: string -> unit}; + +fun drop_newline s = + if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) + else s; + +fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text = + let + val _ = Secure.deny_ml (); + + val current_line = Unsynchronized.ref line; + val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text)); + val out_buffer = Unsynchronized.ref ([]: string list); + fun output () = drop_newline (implode (rev (! out_buffer))); + + fun get () = + (case ! in_buffer of + [] => NONE + | c :: cs => + (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); + fun put s = out_buffer := s :: ! out_buffer; + fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} = + (put (if hard then "Error: " else "Warning: "); + PolyML.prettyPrint (put, 76) msg1; + (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); + put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n")); + + val parameters = + [PolyML.Compiler.CPOutStream put, + PolyML.Compiler.CPNameSpace name_space, + PolyML.Compiler.CPErrorMessageProc put_message, + PolyML.Compiler.CPLineNo (fn () => ! current_line), + PolyML.Compiler.CPFileName file, + PolyML.Compiler.CPPrintInAlphabeticalOrder false] @ + ML_Compiler_Parameters.debug debug; + val _ = + (while not (List.null (! in_buffer)) do + PolyML.compiler (get, parameters) ()) + handle exn => + if Exn.is_interrupt exn then reraise exn + else + (put ("Exception- " ^ General.exnMessage exn ^ " raised"); + error (output ()); reraise exn); + in if verbose then print (output ()) else () 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 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; + +val {use, use_debug, use_no_debug} = + let + val context: ML_Compiler0.context = + {name_space = ML_Name_Space.global, + 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 + ML_Compiler0.use_operations (fn opt_debug => fn file => + ML_Compiler0.use_file context + {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file + handle ERROR msg => (#print context msg; raise error "ML error")) + end; diff -r dd154240a53c -r b90109b2487c src/Pure/ROOT --- a/src/Pure/ROOT Tue Mar 01 21:10:29 2016 +0100 +++ b/src/Pure/ROOT Tue Mar 01 22:11:36 2016 +0100 @@ -5,11 +5,11 @@ files "RAW/ROOT_polyml-5.6.ML" "RAW/ROOT_polyml.ML" - "RAW/compiler_polyml.ML" "RAW/exn.ML" "RAW/exn_trace.ML" "RAW/exn_trace_raw.ML" "RAW/fixed_int_dummy.ML" + "RAW/ml_compiler0.ML" "RAW/ml_compiler_parameters.ML" "RAW/ml_compiler_parameters_polyml-5.6.ML" "RAW/ml_debugger.ML" @@ -37,11 +37,11 @@ files "RAW/ROOT_polyml-5.6.ML" "RAW/ROOT_polyml.ML" - "RAW/compiler_polyml.ML" "RAW/exn.ML" "RAW/exn_trace.ML" "RAW/exn_trace_raw.ML" "RAW/fixed_int_dummy.ML" + "RAW/ml_compiler0.ML" "RAW/ml_compiler_parameters.ML" "RAW/ml_compiler_parameters_polyml-5.6.ML" "RAW/ml_debugger.ML" diff -r dd154240a53c -r b90109b2487c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Mar 01 21:10:29 2016 +0100 +++ b/src/Pure/ROOT.ML Tue Mar 01 22:11:36 2016 +0100 @@ -36,17 +36,18 @@ val {use, use_debug, use_no_debug} = let - val global_context: use_context = + val context: ML_Compiler0.context = {name_space = ML_Name_Space.global, here = Position.here oo Position.line_file, print = writeln, - error = error} + error = error}; in - use_operations (fn opt_debug => fn file => + ML_Compiler0.use_operations (fn opt_debug => fn file => Position.setmp_thread_data (Position.file_only file) (fn () => - use_file global_context {verbose = true, debug = use_debug_option opt_debug} file - handle ERROR msg => (writeln msg; error "ML error")) ()) + ML_Compiler0.use_file context + {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file + handle ERROR msg => (writeln msg; error "ML error")) ()) end; @@ -228,7 +229,7 @@ use "ML/ml_antiquotation.ML"; val {use, use_debug, use_no_debug} = - use_operations (fn opt_debug => fn file => + 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") diff -r dd154240a53c -r b90109b2487c src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Tue Mar 01 21:10:29 2016 +0100 +++ b/src/Tools/Code/code_runtime.ML Tue Mar 01 22:11:36 2016 +0100 @@ -82,7 +82,7 @@ fun exec ctxt verbose code = (if Config.get ctxt trace then tracing code else (); ML_Context.exec (fn () => - use_text ML_Env.local_context + ML_Compiler0.use_text ML_Env.local_context {line = 0, file = "generated code", verbose = verbose, debug = false} code)); fun value ctxt (get, put, put_ml) (prelude, value) = @@ -509,7 +509,7 @@ fun abort _ = error "Only value bindings allowed."; -val notifying_context : use_context = +val notifying_context : ML_Compiler0.context = {name_space = {lookupVal = #lookupVal ML_Env.local_name_space, lookupType = #lookupType ML_Env.local_name_space, @@ -540,7 +540,7 @@ val thy' = Loaded_Values.put [] thy; val _ = Context.set_thread_data ((SOME o Context.Theory) thy'); val _ = - use_text notifying_context + ML_Compiler0.use_text notifying_context {line = 0, file = Path.implode filepath, verbose = false, debug = false} (File.read filepath); val thy'' = Context.the_theory (Context.the_thread_data ()); diff -r dd154240a53c -r b90109b2487c src/Tools/Spec_Check/spec_check.ML --- a/src/Tools/Spec_Check/spec_check.ML Tue Mar 01 21:10:29 2016 +0100 +++ b/src/Tools/Spec_Check/spec_check.ML Tue Mar 01 22:11:36 2016 +0100 @@ -127,7 +127,7 @@ fun determine_type ctxt s = let val return = Unsynchronized.ref "return" - val use_context : use_context = + val context : ML_Compiler0.context = {name_space = #name_space ML_Env.local_context, here = #here ML_Env.local_context, print = fn r => return := r, @@ -135,7 +135,7 @@ val _ = Context.setmp_thread_data (SOME (Context.Proof ctxt)) (fn () => - use_text use_context + ML_Compiler0.use_text context {line = 0, file = "generated code", verbose = true, debug = false} s) () in Gen_Construction.parse_pred (! return) @@ -145,7 +145,7 @@ fun run_test ctxt s = Context.setmp_thread_data (SOME (Context.Proof ctxt)) (fn () => - use_text ML_Env.local_context + ML_Compiler0.use_text ML_Env.local_context {line = 0, file = "generated code", verbose = false, debug = false} s) (); (*split input into tokens*)