# HG changeset patch # User wenzelm # Date 1438889514 -7200 # Node ID 7bf2188a0998fa8b9e7301764eca77b272052a3f # Parent 4c18d8e4fe149ece4f25b4973445b5ccb2e48c4e evaluate ML expressions within debugger context; redirected writeln/warning for ML compiler; diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Aug 06 20:33:12 2015 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Aug 06 21:31:54 2015 +0200 @@ -209,7 +209,9 @@ let val ([{lines, pos, ...}], thy') = files thy; val source = Input.source true (cat_lines lines) (pos, pos); - val flags = {SML = true, exchange = false, redirect = true, verbose = true}; + val flags = + {SML = true, exchange = false, redirect = true, verbose = true, + writeln = writeln, warning = warning}; in thy' |> Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)) @@ -218,7 +220,11 @@ val _ = Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment" (Parse.ML_source >> (fn source => - let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in + let + val flags = + {SML = true, exchange = true, redirect = false, verbose = true, + writeln = writeln, warning = warning}; + in Toplevel.theory (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) end)); @@ -226,7 +232,11 @@ val _ = Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment" (Parse.ML_source >> (fn source => - let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in + let + val flags = + {SML = false, exchange = true, redirect = false, verbose = true, + writeln = writeln, warning = warning}; + in Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval_source flags source) #> Local_Theory.propagate_ml_env) diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Thu Aug 06 20:33:12 2015 +0200 +++ b/src/Pure/ML/ml_compiler.ML Thu Aug 06 21:31:54 2015 +0200 @@ -6,7 +6,9 @@ signature ML_COMPILER = sig - type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool} + type flags = + {SML: bool, exchange: bool, redirect: bool, verbose: bool, + writeln: string -> unit, warning: string -> unit} val flags: flags val verbose: bool -> flags -> flags val eval: flags -> Position.T -> ML_Lex.token list -> unit @@ -15,11 +17,17 @@ structure ML_Compiler: ML_COMPILER = struct -type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool}; -val flags = {SML = false, exchange = false, redirect = false, verbose = false}; +type flags = + {SML: bool, exchange: bool, redirect: bool, verbose: bool, + writeln: string -> unit, warning: string -> unit}; + +val flags: flags = + {SML = false, exchange = false, redirect = false, verbose = false, + writeln = writeln, warning = warning}; fun verbose b (flags: flags) = - {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b}; + {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b, + writeln = #writeln flags, warning = #warning flags}; fun eval (flags: flags) pos toks = let diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Thu Aug 06 20:33:12 2015 +0200 +++ b/src/Pure/ML/ml_compiler_polyml.ML Thu Aug 06 21:31:54 2015 +0200 @@ -145,15 +145,15 @@ val writeln_buffer = Unsynchronized.ref Buffer.empty; fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); - fun output_writeln () = writeln (trim_line (Buffer.content (! writeln_buffer))); + fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer))); val warnings = Unsynchronized.ref ([]: string list); fun warn msg = Unsynchronized.change warnings (cons msg); - fun output_warnings () = List.app warning (rev (! warnings)); + fun output_warnings () = List.app (#warning flags) (rev (! warnings)); val error_buffer = Unsynchronized.ref Buffer.empty; fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); - fun flush_error () = writeln (Buffer.content (! error_buffer)); + fun flush_error () = #writeln flags (Buffer.content (! error_buffer)); fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer))); fun message {message = msg, hard, location = loc, context = _} = diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Thu Aug 06 20:33:12 2015 +0200 +++ b/src/Pure/ML/ml_env.ML Thu Aug 06 21:31:54 2015 +0200 @@ -12,6 +12,7 @@ val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) -> Context.generic -> Context.generic 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_name_space: ML_Name_Space.T @@ -91,6 +92,22 @@ (* name space *) +fun add_name_space {SML} (space: ML_Name_Space.T) = + Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + let + val (tables', sml_tables') = + (tables, sml_tables) |> (if SML then apsnd else apfst) + (fn (val1, type1, fixity1, structure1, signature1, functor1) => + let + val val2 = fold Symtab.update (#allVal space ()) val1; + val type2 = fold Symtab.update (#allType space ()) type1; + val fixity2 = fold Symtab.update (#allFix space ()) fixity1; + val structure2 = fold Symtab.update (#allStruct space ()) structure1; + val signature2 = fold Symtab.update (#allSig space ()) signature1; + val functor2 = fold Symtab.update (#allFunct space ()) functor1; + in (val2, type2, fixity2, structure2, signature2, functor2) end); + in make_data (bootstrap, tables', sml_tables', breakpoints) end); + fun name_space {SML, exchange} : ML_Name_Space.T = let fun lookup sel1 sel2 name = diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/ML/ml_file.ML --- a/src/Pure/ML/ml_file.ML Thu Aug 06 20:33:12 2015 +0200 +++ b/src/Pure/ML/ml_file.ML Thu Aug 06 21:31:54 2015 +0200 @@ -14,7 +14,9 @@ val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); val provide = Resources.provide (src_path, digest); val source = Input.source true (cat_lines lines) (pos, pos); - val flags = {SML = false, exchange = false, redirect = true, verbose = true}; + val flags = + {SML = false, exchange = false, redirect = true, verbose = true, + writeln = writeln, warning = warning}; in gthy |> ML_Context.exec (fn () => ML_Context.eval_source flags source) diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Thu Aug 06 20:33:12 2015 +0200 +++ b/src/Pure/Tools/debugger.ML Thu Aug 06 21:31:54 2015 +0200 @@ -85,12 +85,37 @@ end; +fun the_debug_state thread_name index = + (case get_debugging () of + [] => error ("Missing debugger information for thread " ^ quote thread_name) + | states => + if index < 0 orelse index >= length states then + error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^ + quote thread_name) + else nth states index); + + (* eval ML *) -fun eval thread_name index SML context expression = (* FIXME *) - writeln_message ("SML = " ^ Markup.print_bool SML ^ - "\ncontext = " ^ context ^ "\nexpression = " ^ expression); +fun eval thread_name index SML txt1 txt2 = + let + fun evaluate verbose = + ML_Context.eval + {SML = SML, exchange = false, redirect = false, verbose = verbose, + writeln = writeln_message, warning = warning_message} + Position.none; + + val debug_state = the_debug_state thread_name index; + val context1 = ML_Context.the_generic_context () + |> Context_Position.set_visible_generic false + |> ML_Env.add_name_space {SML = SML} (ML_Debugger.debug_name_space debug_state); + val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); + in + if null (filter_out (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1) + then Context.setmp_thread_data (SOME context1) (fn () => evaluate true toks2) () + else error "FIXME" + end; (* debugger entry point *) diff -r 4c18d8e4fe14 -r 7bf2188a0998 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Thu Aug 06 20:33:12 2015 +0200 +++ b/src/Pure/context_position.ML Thu Aug 06 21:31:54 2015 +0200 @@ -9,6 +9,7 @@ val is_visible_generic: Context.generic -> bool val is_visible: Proof.context -> bool val is_visible_global: theory -> bool + val set_visible_generic: bool -> Context.generic -> Context.generic val set_visible: bool -> Proof.context -> Proof.context val set_visible_global: bool -> theory -> theory val is_really_visible: Proof.context -> bool @@ -40,6 +41,7 @@ val is_visible = is_visible_generic o Context.Proof; val is_visible_global = is_visible_generic o Context.Theory; +val set_visible_generic = Data.map o apsnd o K o SOME; val set_visible = Context.proof_map o Data.map o apsnd o K o SOME; val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME;