# HG changeset patch # User wenzelm # Date 1395952725 -3600 # Node ID 4d8955cdfb9798268bb99ad9cd4dac8b336b8e74 # Parent 801a72ad52d399a631de6fb99bbad0a44d83443a# Parent 5003ea266aef5b4783b7d7b9e68ec3150c00e514 merged diff -r 801a72ad52d3 -r 4d8955cdfb97 NEWS --- a/NEWS Wed Mar 26 11:05:25 2014 -0700 +++ b/NEWS Thu Mar 27 21:38:45 2014 +0100 @@ -541,6 +541,9 @@ *** ML *** +* Moved ML_Compiler.exn_trace and other operations on exceptions to +structure Runtime. Minor INCOMPATIBILITY. + * Discontinued old Toplevel.debug in favour of system option "ML_exception_trace", which may be also declared within the context via "declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY. diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Doc/IsarImplementation/ML.thy --- a/src/Doc/IsarImplementation/ML.thy Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Doc/IsarImplementation/ML.thy Thu Mar 27 21:38:45 2014 +0100 @@ -1163,7 +1163,7 @@ @{index_ML_exception Fail: string} \\ @{index_ML Exn.is_interrupt: "exn -> bool"} \\ @{index_ML reraise: "exn -> 'a"} \\ - @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\ + @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\ \end{mldecls} \begin{description} @@ -1191,12 +1191,12 @@ while preserving its implicit position information (if possible, depending on the ML platform). - \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text + \item @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~@{text "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing a full trace of its stack of nested exceptions (if possible, depending on the ML platform). - Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is + Inserting @{ML Runtime.exn_trace} into ML code temporarily is useful for debugging, but not suitable for production code. \end{description} diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Doc/antiquote_setup.ML Thu Mar 27 21:38:45 2014 +0100 @@ -100,8 +100,7 @@ val txt' = if kind = "" then txt else kind ^ " " ^ txt; val _ = - ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1) - (ml (toks1, toks2)); + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2)); val kind' = if kind = "" then "ML" else "ML " ^ kind; in "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ @@ -192,17 +191,17 @@ fun no_check _ _ = true; -fun check_command (name, pos) = +fun check_command ctxt (name, pos) = is_some (Keyword.command_keyword name) andalso let val markup = Outer_Syntax.scan Position.none name |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ()))) |> map (snd o fst); - val _ = List.app (Position.report pos) markup; + val _ = Context_Position.reports ctxt (map (pair pos) markup); in true end; -fun check_tool (name, pos) = +fun check_tool ctxt (name, pos) = let fun tool dir = let val path = Path.append dir (Path.basic name) @@ -210,7 +209,7 @@ in (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of NONE => false - | SOME path => (Position.report pos (Markup.path (Path.implode path)); true)) + | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true)) end; val arg = enclose "{" "}" o clean_string; @@ -255,7 +254,7 @@ val _ = Theory.setup (entity_antiqs no_check "" @{binding syntax} #> - entity_antiqs (K check_command) "isacommand" @{binding command} #> + entity_antiqs check_command "isacommand" @{binding command} #> entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #> entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #> entity_antiqs (can o Method.check_name) "" @{binding method} #> @@ -269,7 +268,7 @@ entity_antiqs no_check "isatt" @{binding system_option} #> entity_antiqs no_check "" @{binding inference} #> entity_antiqs no_check "isatt" @{binding executable} #> - entity_antiqs (K check_tool) "isatool" @{binding tool} #> + entity_antiqs check_tool "isatool" @{binding tool} #> entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #> entity_antiqs (K (is_action o #1)) "isatt" @{binding action}); diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/TPTP/TPTP_Interpret_Test.thy --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Thu Mar 27 21:38:45 2014 +0100 @@ -132,7 +132,7 @@ if Exn.is_interrupt exn then reraise exn else (warning (" test: file " ^ Path.print file ^ - " raised exception: " ^ ML_Compiler.exn_message exn); + " raised exception: " ^ Runtime.exn_message exn); {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime}) val to_real = Time.toReal val diff_elapsed = diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/TPTP/TPTP_Test.thy --- a/src/HOL/TPTP/TPTP_Test.thy Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/TPTP/TPTP_Test.thy Thu Mar 27 21:38:45 2014 +0100 @@ -63,7 +63,7 @@ reraise exn else (report ctxt (msg ^ " test: file " ^ Path.print file_name ^ - " raised exception: " ^ ML_Compiler.exn_message exn); + " raised exception: " ^ Runtime.exn_message exn); default_val) end diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/Tools/SMT/smt_config.ML Thu Mar 27 21:38:45 2014 +0100 @@ -101,8 +101,9 @@ filter (is_available ctxt) (all_solvers_of ctxt) fun warn_solver (Context.Proof ctxt) name = - Context_Position.if_visible ctxt + if Context_Position.is_visible ctxt then warning ("The SMT solver " ^ quote name ^ " is not installed.") + else () | warn_solver _ _ = (); fun select_solver name context = diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/Tools/SMT2/smt2_config.ML --- a/src/HOL/Tools/SMT2/smt2_config.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/Tools/SMT2/smt2_config.ML Thu Mar 27 21:38:45 2014 +0100 @@ -99,8 +99,9 @@ filter (is_available ctxt) (all_solvers_of ctxt) fun warn_solver (Context.Proof ctxt) name = - Context_Position.if_visible ctxt + if Context_Position.is_visible ctxt then warning ("The SMT solver " ^ quote name ^ " is not installed.") + else () | warn_solver _ _ = (); fun select_solver name context = diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/Tools/Sledgehammer/async_manager.ML --- a/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Thu Mar 27 21:38:45 2014 +0100 @@ -130,7 +130,7 @@ fun check_thread_manager () = Synchronized.change global_state (fn state as {manager, timeout_heap, active, canceling, messages, store} => if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state - else let val manager = SOME (Toplevel.thread false (fn () => + else let val manager = SOME (Runtime.thread false (fn () => let fun time_limit timeout_heap = (case try Thread_Heap.min timeout_heap of @@ -183,7 +183,7 @@ fun thread tool birth_time death_time desc f = - (Toplevel.thread true + (Runtime.thread true (fn () => let val self = Thread.self () diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Mar 27 21:38:45 2014 +0100 @@ -157,7 +157,7 @@ reraise exn else (unknownN, fn () => "Internal error:\n" ^ - ML_Compiler.exn_message exn ^ "\n")) + Runtime.exn_message exn ^ "\n")) val _ = (* The "expect" argument is deliberately ignored if the prover is missing so that the "Metis_Examples" can be processed on any diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 27 21:38:45 2014 +0100 @@ -337,7 +337,7 @@ else (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ - ML_Compiler.exn_message exn); def) + Runtime.exn_message exn); def) fun graph_info G = string_of_int (length (Graph.keys G)) ^ " node(s), " ^ diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Mar 27 21:38:45 2014 +0100 @@ -159,7 +159,7 @@ |> (fn {outcome, used_facts} => (outcome, used_facts)) handle exn => if Exn.is_interrupt exn then reraise exn - else (ML_Compiler.exn_message exn |> SMT_Failure.Other_Failure |> SOME, []) + else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, []) val death = Timer.checkRealTimer timer val outcome0 = if is_none outcome0 then SOME outcome else outcome0 diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 27 21:38:45 2014 +0100 @@ -160,7 +160,7 @@ if Exn.is_interrupt exn orelse debug then reraise exn else - {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)), + {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)), rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []} diff -r 801a72ad52d3 -r 4d8955cdfb97 src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Wed Mar 26 11:05:25 2014 -0700 +++ b/src/HOL/ex/Cartouche_Examples.thy Thu Mar 27 21:38:45 2014 +0100 @@ -120,7 +120,7 @@ ML_Lex.read Position.none "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read Position.none ");"; - val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks; + val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks; in "" end); *} diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/General/completion.ML --- a/src/Pure/General/completion.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/General/completion.ML Thu Mar 27 21:38:45 2014 +0100 @@ -10,7 +10,6 @@ val names: Position.T -> (string * (string * string)) list -> T val none: T val reported_text: T -> string - val report: T -> unit val suppress_abbrevs: string -> Markup.T list end; @@ -46,8 +45,6 @@ else "" end; -val report = Output.report o reported_text; - (* suppress short abbreviations *) diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/General/output.ML diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/attrib.ML Thu Mar 27 21:38:45 2014 +0100 @@ -457,9 +457,9 @@ register_config Name_Space.names_long_raw #> register_config Name_Space.names_short_raw #> register_config Name_Space.names_unique_raw #> - register_config ML_Context.source_trace_raw #> - register_config ML_Compiler.print_depth_raw #> - register_config Runtime.exception_trace_raw #> + register_config ML_Options.source_trace_raw #> + register_config ML_Options.exception_trace_raw #> + register_config ML_Options.print_depth_raw #> register_config Proof_Context.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> register_config Goal_Display.show_main_goal_raw #> diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/generic_target.ML Thu Mar 27 21:38:45 2014 +0100 @@ -57,12 +57,13 @@ fun check_mixfix ctxt (b, extra_tfrees) mx = if null extra_tfrees then mx else - (Context_Position.if_visible ctxt warning - ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ - commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^ - (if mx = NoSyn then "" - else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))); - NoSyn); + (if Context_Position.is_visible ctxt then + warning + ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ + commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^ + (if mx = NoSyn then "" + else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))) + else (); NoSyn); fun check_mixfix_global (b, no_params) mx = if no_params orelse mx = NoSyn then mx diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/isar_cmd.ML Thu Mar 27 21:38:45 2014 +0100 @@ -145,8 +145,10 @@ \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\ \end;\n"); - val flags = {SML = false, verbose = false}; - in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end; + in + Context.theory_map + (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants)) + end; (* old-style defs *) @@ -236,10 +238,12 @@ ); fun ml_diag verbose source = Toplevel.keep (fn state => - let val opt_ctxt = - try Toplevel.generic_theory_of state - |> Option.map (Context.proof_of #> Diag_State.put state) - in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end); + let + val opt_ctxt = + try Toplevel.generic_theory_of state + |> Option.map (Context.proof_of #> Diag_State.put state); + val flags = ML_Compiler.verbose verbose ML_Compiler.flags; + in ML_Context.eval_source_in opt_ctxt flags source end); val diag_state = Diag_State.get; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/isar_syn.ML Thu Mar 27 21:38:45 2014 +0100 @@ -273,23 +273,26 @@ let val ([{lines, pos, ...}], thy') = files thy; val source = {delimited = true, text = cat_lines lines, pos = pos}; + val flags = {SML = true, redirect = true, verbose = true}; in thy' |> Context.theory_map - (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source)) + (ML_Context.exec (fn () => ML_Context.eval_source flags source)) end))); val _ = Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory" (Parse.ML_source >> (fn source => Toplevel.generic_theory - (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #> + (ML_Context.exec (fn () => + ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #> Local_Theory.propagate_ml_env))); val _ = Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map - (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #> + (ML_Context.exec (fn () => + ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> Proof.propagate_ml_env))); val _ = diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/outer_syntax.ML Thu Mar 27 21:38:45 2014 +0100 @@ -143,7 +143,8 @@ fun add_command (name, kind) cmd = CRITICAL (fn () => let - val thy = ML_Context.the_global_context (); + val context = ML_Context.the_generic_context (); + val thy = Context.theory_of context; val Command {pos, ...} = cmd; val _ = (case try (Thy_Header.the_keyword thy) name of @@ -155,7 +156,7 @@ if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind) else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos)); - val _ = Position.report pos (command_markup true (name, cmd)); + val _ = Context_Position.report_generic context pos (command_markup true (name, cmd)); fun redefining () = "Redefining outer syntax command " ^ quote name ^ Position.here (Position.thread_data ()); diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 27 21:38:45 2014 +0100 @@ -718,7 +718,7 @@ fun check_tfree ctxt v = let val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v]; - val _ = Context_Position.if_visible ctxt Output.report sorting_report; + val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else (); in a end; end; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/runtime.ML Thu Mar 27 21:38:45 2014 +0100 @@ -11,16 +11,17 @@ exception EXCURSION_FAIL of exn * string exception TOPLEVEL_ERROR val exn_context: Proof.context option -> exn -> exn - type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T} type error = ((serial * string) * string option) - val exn_messages_ids: exn_info -> exn -> error list - val exn_messages: exn_info -> exn -> (serial * string) list - val exn_message: exn_info -> exn -> string - val exception_trace_raw: Config.raw - val exception_trace: bool Config.T - val debugging: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b - val controlled_execution: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b + val exn_messages_ids: exn -> error list + val exn_messages: exn -> (serial * string) list + val exn_message: exn -> string + val exn_error_message: exn -> unit + val exn_trace: (unit -> 'a) -> 'a + val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b + val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b + val toplevel_program: (unit -> 'a) -> 'a + val thread: bool -> (unit -> unit) -> Thread.thread end; structure Runtime: RUNTIME = @@ -44,7 +45,6 @@ (* exn_message *) -type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T}; type error = ((serial * string) * string option); local @@ -75,10 +75,10 @@ in -fun exn_messages_ids {exn_position, pretty_exn} e = +fun exn_messages_ids e = let fun raised exn name msgs = - let val pos = Position.here (exn_position exn) in + let val pos = Position.here (Exn_Output.position exn) in (case msgs of [] => "exception " ^ name ^ " raised" ^ pos | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg @@ -117,7 +117,7 @@ | THM (msg, i, thms) => raised exn ("THM " ^ string_of_int i) (msg :: robust_context context Display.string_of_thm thms) - | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []); + | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []); in [((i, msg), id)] end) and sorted_msgs context exn = sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn)); @@ -126,30 +126,27 @@ end; -fun exn_messages exn_info exn = map #1 (exn_messages_ids exn_info exn); +fun exn_messages exn = map #1 (exn_messages_ids exn); -fun exn_message exn_info exn = - (case exn_messages exn_info exn of +fun exn_message exn = + (case exn_messages exn of [] => "Interrupt" | msgs => cat_lines (map snd msgs)); +val exn_error_message = Output.error_message o exn_message; +fun exn_trace e = print_exception_trace exn_message e; + + (** controlled execution **) -val exception_trace_raw = Config.declare_option "ML_exception_trace"; -val exception_trace = Config.bool exception_trace_raw; - -fun exception_trace_enabled NONE = - (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false) - | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace; - -fun debugging exn_message opt_context f x = - if exception_trace_enabled opt_context +fun debugging opt_context f x = + if ML_Options.exception_trace_enabled opt_context then print_exception_trace exn_message (fn () => f x) else f x; -fun controlled_execution exn_message opt_context f x = - (f |> debugging exn_message opt_context |> Future.interruptible_task) x; +fun controlled_execution opt_context f x = + (f |> debugging opt_context |> Future.interruptible_task) x; fun toplevel_error output_exn f x = f x handle exn => @@ -163,5 +160,17 @@ val _ = output_exn (exn_context opt_ctxt exn); in raise TOPLEVEL_ERROR end; +fun toplevel_program body = + (body |> controlled_execution NONE |> toplevel_error exn_error_message) (); + +(*Proof General legacy*) +fun thread interrupts body = + Thread.fork + (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn) + |> debugging NONE + |> toplevel_error + (fn exn => Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn))), + Simple_Thread.attributes interrupts); + end; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/toplevel.ML Thu Mar 27 21:38:45 2014 +0100 @@ -29,10 +29,6 @@ val interact: bool Unsynchronized.ref val timing: bool Unsynchronized.ref val profiling: int Unsynchronized.ref - val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b - val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b - val program: (unit -> 'a) -> 'a - val thread: bool -> (unit -> unit) -> Thread.thread type transition val empty: transition val print_of: transition -> bool @@ -232,26 +228,6 @@ val profiling = Unsynchronized.ref 0; -(* controlled execution *) - -fun debugging arg = Runtime.debugging ML_Compiler.exn_message arg; -fun controlled_execution arg = Runtime.controlled_execution ML_Compiler.exn_message arg; - -fun program body = - (body - |> controlled_execution NONE - |> Runtime.toplevel_error ML_Compiler.exn_error_message) (); - -fun thread interrupts body = - Thread.fork - (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn) - |> debugging NONE - |> Runtime.toplevel_error - (fn exn => - Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))), - Simple_Thread.attributes interrupts); - - (* node transactions -- maintaining stable checkpoints *) exception FAILURE of state * exn; @@ -275,7 +251,7 @@ val (result, err) = cont_node - |> controlled_execution (SOME context) f + |> Runtime.controlled_execution (SOME context) f |> state_error NONE handle exn => state_error (SOME exn) cont_node; in @@ -304,11 +280,11 @@ local fun apply_tr _ (Init f) (State (NONE, _)) = - State (SOME (Theory (Context.Theory (controlled_execution NONE f ()), NONE)), NONE) + State (SOME (Theory (Context.Theory (Runtime.controlled_execution NONE f ()), NONE)), NONE) | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) = exit_transaction state | apply_tr int (Keep f) state = - controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state + Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state | apply_tr int (Transaction (f, g)) (State (SOME state, _)) = apply_transaction (fn x => f int x) g state | apply_tr _ _ _ = raise UNDEF; @@ -649,8 +625,8 @@ fun command_errors int tr st = (case transition int tr st of SOME (st', NONE) => ([], SOME st') - | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE) - | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE)); + | SOME (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE) + | NONE => (Runtime.exn_messages_ids Runtime.TERMINATE, NONE)); fun command_exception int tr st = (case transition int tr st of diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Isar/typedecl.ML Thu Mar 27 21:38:45 2014 +0100 @@ -102,11 +102,12 @@ val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs; val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs []; val _ = - if null ignored then () - else Context_Position.if_visible ctxt warning - ("Ignoring sort constraints in type variables(s): " ^ - commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^ - "\nin type abbreviation " ^ Binding.print b); + if not (null ignored) andalso Context_Position.is_visible ctxt then + warning + ("Ignoring sort constraints in type variables(s): " ^ + commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^ + "\nin type abbreviation " ^ Binding.print b) + else (); in rhs end; in diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/ML-Systems/polyml.ML Thu Mar 27 21:38:45 2014 +0100 @@ -175,5 +175,5 @@ ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); val ml_make_string = - "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))"; + "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))"; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML/exn_output.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/exn_output.ML Thu Mar 27 21:38:45 2014 +0100 @@ -0,0 +1,20 @@ +(* Title: Pure/ML/exn_output.ML + Author: Makarius + +Auxiliary operations for exception output -- generic version. +*) + +signature EXN_OUTPUT = +sig + val position: exn -> Position.T + val pretty: exn -> Pretty.T +end + +structure Exn_Output: EXN_OUTPUT = +struct + +fun position (_: exn) = Position.none +val pretty = Pretty.str o General.exnMessage; + +end; + diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML/exn_output_polyml.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/exn_output_polyml.ML Thu Mar 27 21:38:45 2014 +0100 @@ -0,0 +1,19 @@ +(* Title: Pure/ML/exn_output_polyml.ML + Author: Makarius + +Auxiliary operations for exception output -- Poly/ML version. +*) + +structure Exn_Output: EXN_OUTPUT = +struct + +fun position exn = + (case PolyML.exceptionLocation exn of + NONE => Position.none + | SOME loc => Exn_Properties.position_of loc); + +fun pretty (exn: exn) = + Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ()))); + +end; + diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML/exn_properties_polyml.ML --- a/src/Pure/ML/exn_properties_polyml.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/ML/exn_properties_polyml.ML Thu Mar 27 21:38:45 2014 +0100 @@ -6,7 +6,7 @@ signature EXN_PROPERTIES = sig - val of_location: PolyML.location -> Properties.T + val position_of: PolyML.location -> Position.T val get: exn -> Properties.T val update: Properties.entry list -> exn -> exn end; @@ -14,23 +14,35 @@ structure Exn_Properties: EXN_PROPERTIES = struct -fun of_location (loc: PolyML.location) = +(* source locations *) + +fun props_of (loc: PolyML.location) = (case YXML.parse_body (#file loc) of [] => [] | [XML.Text file] => [(Markup.fileN, file)] | body => XML.Decode.properties body); +fun position_of loc = + Position.make + {line = #startLine loc, + offset = #startPosition loc, + end_offset = #endPosition loc, + props = props_of loc}; + + +(* exception properties *) + fun get exn = (case PolyML.exceptionLocation exn of NONE => [] - | SOME loc => of_location loc); + | SOME loc => props_of loc); fun update entries exn = let val loc = the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} (PolyML.exceptionLocation exn); - val props = of_location loc; + val props = props_of loc; val props' = fold Properties.put entries props; in if props = props' then exn diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/ML/ml_compiler.ML Thu Mar 27 21:38:45 2014 +0100 @@ -1,63 +1,31 @@ (* Title: Pure/ML/ml_compiler.ML Author: Makarius -Runtime compilation -- generic version. +Runtime compilation and evaluation -- generic version. *) signature ML_COMPILER = sig - val exn_messages_ids: exn -> Runtime.error list - val exn_messages: exn -> (serial * string) list - val exn_message: exn -> string - val exn_error_message: exn -> unit - val exn_trace: (unit -> 'a) -> 'a - val print_depth_raw: Config.raw - val print_depth: int Config.T - val get_print_depth: unit -> int - type flags = {SML: bool, verbose: bool} + type flags = {SML: bool, redirect: bool, verbose: bool} + val flags: flags + val verbose: bool -> flags -> flags val eval: flags -> Position.T -> ML_Lex.token list -> unit end structure ML_Compiler: ML_COMPILER = struct -(* exceptions *) - -val exn_info = - {exn_position = fn _: exn => Position.none, - pretty_exn = Pretty.str o General.exnMessage}; - -val exn_messages_ids = Runtime.exn_messages_ids exn_info; -val exn_messages = Runtime.exn_messages exn_info; -val exn_message = Runtime.exn_message exn_info; - -val exn_error_message = Output.error_message o exn_message; -fun exn_trace e = print_exception_trace exn_message e; - - -(* print depth *) +type flags = {SML: bool, redirect: bool, verbose: bool}; +val flags = {SML = false, redirect = false, verbose = false}; +fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v}; -val print_depth_raw = - Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ())); -val print_depth = Config.int print_depth_raw; - -fun get_print_depth () = - (case Context.thread_data () of - NONE => get_default_print_depth () - | SOME context => Config.get_generic context print_depth); - - -(* eval *) - -type flags = {SML: bool, verbose: bool}; - -fun eval {SML, verbose} pos toks = +fun eval (flags: flags) pos toks = let - val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else (); + val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else (); val line = the_default 1 (Position.line_of pos); val file = the_default "ML" (Position.file_of pos); val text = ML_Lex.flatten toks; - in Secure.use_text ML_Env.local_context (line, file) verbose text end; + in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end; end; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/ML/ml_compiler_polyml.ML Thu Mar 27 21:38:45 2014 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/ML/ml_compiler_polyml.ML Author: Makarius -Advanced runtime compilation for Poly/ML. +Runtime compilation and evaluation -- Poly/ML version. *) structure ML_Compiler: ML_COMPILER = @@ -10,77 +10,67 @@ open ML_Compiler; -(* source locations *) - -fun position_of (loc: PolyML.location) = - let - val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc; - val props = Exn_Properties.of_location loc; - in - Position.make {line = line, offset = offset, end_offset = end_offset, props = props} - end; - - -(* exn_info *) - -fun exn_position exn = - (case PolyML.exceptionLocation exn of - NONE => Position.none - | SOME loc => position_of loc); - -fun pretty_exn (exn: exn) = - Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ()))); - -val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn}; - - -(* exn_message *) - -val exn_messages_ids = Runtime.exn_messages_ids exn_info; -val exn_messages = Runtime.exn_messages exn_info; -val exn_message = Runtime.exn_message exn_info; - -val exn_error_message = Output.error_message o exn_message; -fun exn_trace e = print_exception_trace exn_message e; - - (* parse trees *) -fun report_parse_tree depth space = +fun report_parse_tree redirect depth space parse_tree = let - val reported_text = + val is_visible = (case Context.thread_data () of - SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt - | _ => Position.reported_text); + SOME context => Context_Position.is_visible_generic context + | NONE => true); + fun is_reported pos = is_visible andalso Position.is_reported pos; + + fun reported_types loc types = + let val pos = Exn_Properties.position_of loc in + is_reported pos ? + let + val xml = + PolyML.NameSpace.displayTypeExpression (types, depth, space) + |> pretty_ml |> Pretty.from_ML |> Pretty.string_of + |> Output.output |> YXML.parse_body; + in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end + end; fun reported_entity kind loc decl = - reported_text (position_of loc) - (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) ""; + let val pos = Exn_Properties.position_of loc in + is_reported pos ? + let + val def_pos = Exn_Properties.position_of decl; + fun markup () = + (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos); + in cons (pos, markup, fn () => "") end + end; - fun reported loc (PolyML.PTtype types) = - cons - (PolyML.NameSpace.displayTypeExpression (types, depth, space) - |> pretty_ml |> Pretty.from_ML |> Pretty.string_of - |> reported_text (position_of loc) Markup.ML_typing) - | reported loc (PolyML.PTdeclaredAt decl) = - cons (reported_entity Markup.ML_defN loc decl) - | reported loc (PolyML.PTopenedAt decl) = - cons (reported_entity Markup.ML_openN loc decl) - | reported loc (PolyML.PTstructureAt decl) = - cons (reported_entity Markup.ML_structureN loc decl) + fun reported loc (PolyML.PTtype types) = reported_types loc types + | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl + | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl + | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) | reported _ _ = I and reported_tree (loc, props) = fold (reported loc) props; - in fn tree => Output.report (implode (reported_tree tree [])) end; + + val persistent_reports = reported_tree parse_tree []; + + fun output () = + persistent_reports + |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ())) + |> implode |> Output.report; + in + if not (null persistent_reports) andalso redirect andalso Multithreading.enabled () + then + Execution.print + {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output + else output () + end; (* eval ML source tokens *) -fun eval {SML, verbose} pos toks = +fun eval (flags: flags) pos toks = let val _ = Secure.secure_mltext (); - val space = if SML then ML_Env.SML_name_space else ML_Env.name_space; + val space = if #SML flags then ML_Env.SML_name_space else ML_Env.name_space; val opt_context = Context.thread_data (); @@ -122,7 +112,7 @@ fun message {message = msg, hard, location = loc, context = _} = let - val pos = position_of loc; + val pos = Exn_Properties.position_of loc; val txt = (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ Pretty.string_of (Pretty.from_ML (pretty_ml msg)); @@ -131,7 +121,7 @@ (* results *) - val depth = get_print_depth (); + val depth = ML_Options.get_print_depth (); fun apply_result {fixes, types, signatures, structures, functors, values} = let @@ -166,14 +156,14 @@ fun result_fun (phase1, phase2) () = ((case phase1 of NONE => () - | SOME parse_tree => report_parse_tree depth space parse_tree); + | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree); (case phase2 of NONE => raise STATIC_ERRORS () | SOME code => apply_result ((code - |> Runtime.debugging exn_message opt_context - |> Runtime.toplevel_error (err o exn_message)) ()))); + |> Runtime.debugging opt_context + |> Runtime.toplevel_error (err o Runtime.exn_message)) ()))); (* compiler invocation *) @@ -185,7 +175,7 @@ PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), PolyML.Compiler.CPFileName location_props, - PolyML.Compiler.CPPrintDepth get_print_depth, + PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth, PolyML.Compiler.CPCompilerResultFun result_fun, PolyML.Compiler.CPPrintInAlphabeticalOrder false]; val _ = @@ -199,12 +189,12 @@ (case exn of STATIC_ERRORS () => "" | Runtime.TOPLEVEL_ERROR => "" - | _ => "Exception- " ^ Pretty.string_of (pretty_exn exn) ^ " raised"); + | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised"); val _ = output_warnings (); val _ = output_writeln (); in raise_error exn_msg end; in - if verbose then (output_warnings (); flush_error (); output_writeln ()) + if #verbose flags then (output_warnings (); flush_error (); output_writeln ()) else () end; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/ML/ml_context.ML Thu Mar 27 21:38:45 2014 +0100 @@ -17,8 +17,6 @@ val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) -> theory -> theory val print_antiquotations: Proof.context -> unit - val source_trace_raw: Config.raw - val source_trace: bool Config.T val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T -> Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit @@ -137,21 +135,17 @@ in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end; in ((ml_env @ end_env, ml_body), opt_ctxt') end; -val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false); -val source_trace = Config.bool source_trace_raw; - fun eval flags pos ants = let - val non_verbose = {SML = #SML flags, verbose = false}; + val non_verbose = ML_Compiler.verbose false flags; (*prepare source text*) val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ()); val _ = (case Option.map Context.proof_of env_ctxt of SOME ctxt => - if Config.get ctxt source_trace then - Context_Position.if_visible ctxt - tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body]) + if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt + then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body]) else () | NONE => ()); @@ -187,13 +181,14 @@ (fn () => eval_source flags source) (); fun expression pos bind body ants = - exec (fn () => eval {SML = false, verbose = false} pos - (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @ + exec (fn () => + eval ML_Compiler.flags pos + (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @ ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));"))); end; fun use s = - ML_Context.eval_file {SML = false, verbose = true} (Path.explode s) + ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s) handle ERROR msg => (writeln msg; error "ML error"); diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML/ml_options.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_options.ML Thu Mar 27 21:38:45 2014 +0100 @@ -0,0 +1,49 @@ +(* Title: Pure/ML/ml_options.ML + Author: Makarius + +ML configuration options. +*) + +signature ML_OPTIONS = +sig + val source_trace_raw: Config.raw + val source_trace: bool Config.T + val exception_trace_raw: Config.raw + val exception_trace: bool Config.T + val exception_trace_enabled: Context.generic option -> bool + val print_depth_raw: Config.raw + val print_depth: int Config.T + val get_print_depth: unit -> int +end; + +structure ML_Options: ML_OPTIONS = +struct + +(* source trace *) + +val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false); +val source_trace = Config.bool source_trace_raw; + + +(* exception trace *) + +val exception_trace_raw = Config.declare_option "ML_exception_trace"; +val exception_trace = Config.bool exception_trace_raw; + +fun exception_trace_enabled NONE = + (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false) + | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace; + + +(* print depth *) + +val print_depth_raw = + Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ())); +val print_depth = Config.int print_depth_raw; + +fun get_print_depth () = + (case Context.thread_data () of + NONE => get_default_print_depth () + | SOME context => Config.get_generic context print_depth); + +end; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/ML/ml_thms.ML Thu Mar 27 21:38:45 2014 +0100 @@ -130,7 +130,7 @@ else if not (ML_Syntax.is_identifier name) then error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") else - ML_Compiler.eval {SML = false, verbose = true} Position.none + ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); val _ = Theory.setup (Stored_Thms.put []); in () end; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/command.ML Thu Mar 27 21:38:45 2014 +0100 @@ -20,7 +20,7 @@ eval -> print list -> print list option type print_fn = Toplevel.transition -> Toplevel.state -> unit type print_function = - {command_name: string, args: string list} -> + {command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option val print_function: string -> print_function -> unit val no_print_function: string -> unit @@ -172,9 +172,10 @@ datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo}; -fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id'; +fun eval_exec_id (Eval {exec_id, ...}) = exec_id; +val eval_eq = op = o pairself eval_exec_id; -fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id; +val eval_running = Execution.is_running_exec o eval_exec_id; fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process; fun eval_result (Eval {eval_process, ...}) = memo_result eval_process; @@ -195,7 +196,7 @@ (Thy_Output.check_text (Token.source_position_of cmt) st'; []) handle exn => if Exn.is_interrupt exn then reraise exn - else ML_Compiler.exn_messages_ids exn)) (); + else Runtime.exn_messages_ids exn)) (); fun report tr m = Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) (); @@ -260,10 +261,13 @@ {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool, exec_id: Document_ID.exec, print_process: unit memo}; +fun print_exec_id (Print {exec_id, ...}) = exec_id; +val print_eq = op = o pairself print_exec_id; + type print_fn = Toplevel.transition -> Toplevel.state -> unit; type print_function = - {command_name: string, args: string list} -> + {command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option; local @@ -272,12 +276,10 @@ Synchronized.var "Command.print_functions" ([]: (string * print_function) list); fun print_error tr opt_context e = - (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution opt_context) e () + (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e () handle exn => if Exn.is_interrupt exn then reraise exn - else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn); - -fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id'; + else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn); fun print_finished (Print {print_process, ...}) = memo_finished print_process; @@ -315,9 +317,9 @@ fun new_print name args get_pr = let - val params = {command_name = command_name, args = args}; + val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval}; in - (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of + (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of Exn.Res NONE => NONE | Exn.Res (SOME pr) => SOME (make_print name args pr) | Exn.Exn exn => SOME (bad_print name args exn)) @@ -353,6 +355,14 @@ end; val _ = + print_function "Execution.print" + (fn {args, exec_id, ...} => + if null args then + SOME {delay = NONE, pri = 1, persistent = false, strict = true, + print_fn = fn _ => fn _ => Execution.fork_prints exec_id} + else NONE); + +val _ = print_function "print_state" (fn {command_name, ...} => SOME {delay = NONE, pri = 1, persistent = false, strict = true, @@ -373,8 +383,7 @@ (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []); fun exec_ids NONE = [] - | exec_ids (SOME (Eval {exec_id, ...}, prints)) = - exec_id :: map (fn Print {exec_id, ...} => exec_id) prints; + | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints; local diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/command.scala Thu Mar 27 21:38:45 2014 +0100 @@ -27,8 +27,8 @@ { type Entry = (Long, XML.Tree) val empty = new Results(SortedMap.empty) - def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _) - def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _) + def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _) + def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _) } final class Results private(private val rep: SortedMap[Long, XML.Tree]) @@ -81,11 +81,6 @@ def add(index: Markup_Index, markup: Text.Markup): Markups = new Markups(rep + (index -> (this(index) + markup))) - def ++ (other: Markups): Markups = - new Markups( - (rep.keySet ++ other.rep.keySet) - .map(index => index -> (this(index) ++ other(index))).toMap) - override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { @@ -98,6 +93,16 @@ /* state */ + object State + { + def merge_results(states: List[State]): Command.Results = + Results.merge(states.map(_.results)) + + def merge_markup(states: List[State], index: Markup_Index, + range: Text.Range, elements: Document.Elements): Markup_Tree = + Markup_Tree.merge(states.map(_.markup(index)), range, elements) + } + sealed case class State( command: Command, status: List[Markup] = Nil, @@ -108,9 +113,6 @@ def markup(index: Markup_Index): Markup_Tree = markups(index) - def markup_to_XML(filter: XML.Elem => Boolean): XML.Body = - markup(Markup_Index.markup).to_XML(command.range, command.source, filter) - /* content */ @@ -132,7 +134,7 @@ copy(markups = markups1.add(Markup_Index(false, file_name), m)) } - def + (alt_id: Document_ID.Generic, message: XML.Elem): State = + def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State = message match { case XML.Elem(Markup(Markup.STATUS, _), msgs) => (this /: msgs)((state, msg) => @@ -154,7 +156,7 @@ msg match { case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, symbol_range)), args) - if id == command.id || id == alt_id => + if valid_id(id) => command.chunks.get(file_name) match { case Some(chunk) => chunk.incorporate(symbol_range) match { @@ -187,7 +189,7 @@ if (Protocol.is_inlined(message)) { for { (file_name, chunk) <- command.chunks - range <- Protocol.message_positions(command.id, alt_id, chunk, message) + range <- Protocol.message_positions(valid_id, chunk, message) } st = st.add_markup(false, file_name, Text.Info(range, message2)) } st @@ -196,14 +198,7 @@ System.err.println("Ignored message without serial number: " + message) this } - } - - def ++ (other: State): State = - copy( - status = other.status ::: status, - results = results ++ other.results, - markups = markups ++ other.markups - ) + } } diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/document.scala Thu Mar 27 21:38:45 2014 +0100 @@ -429,13 +429,13 @@ range: Text.Range, info: A, elements: Elements, - result: Command.State => (A, Text.Markup) => Option[A], + result: Command.Results => (A, Text.Markup) => Option[A], status: Boolean = false): List[Text.Info[A]] def select[A]( range: Text.Range, elements: Elements, - result: Command.State => Text.Markup => Option[A], + result: Command.Results => Text.Markup => Option[A], status: Boolean = false): List[Text.Info[A]] } @@ -521,15 +521,19 @@ def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail) def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) + def valid_id(st: Command.State)(id: Document_ID.Generic): Boolean = + id == st.command.id || + (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false }) + def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) = execs.get(id) match { case Some(st) => - val new_st = st + (id, message) + val new_st = st + (valid_id(st), message) (new_st, copy(execs = execs + (id -> new_st))) case None => commands.get(id) match { case Some(st) => - val new_st = st + (id, message) + val new_st = st + (valid_id(st), message) (new_st, copy(commands = commands + (id -> new_st))) case None => fail } @@ -626,25 +630,37 @@ assignments = assignments1) } - def command_state(version: Version, command: Command): Command.State = + def command_states(version: Version, command: Command): List[Command.State] = { require(is_assigned(version)) try { the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) .map(the_dynamic_state(_)) match { - case eval_state :: print_states => (eval_state /: print_states)(_ ++ _) case Nil => fail + case states => states } } catch { case _: State.Fail => - try { the_static_state(command.id) } - catch { case _: State.Fail => command.init_state } + try { List(the_static_state(command.id)) } + catch { case _: State.Fail => List(command.init_state) } } } - def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body = - node.commands.toList.map(cmd => command_state(version, cmd).markup_to_XML(filter)).flatten + def command_results(version: Version, command: Command): Command.Results = + Command.State.merge_results(command_states(version, command)) + + def command_markup(version: Version, command: Command, index: Command.Markup_Index, + range: Text.Range, elements: Elements): Markup_Tree = + Command.State.merge_markup(command_states(version, command), index, range, elements) + + def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body = + (for { + command <- node.commands.iterator + markup = + command_markup(version, command, Command.Markup_Index.markup, command.range, elements) + tree <- markup.to_XML(command.range, command.source, elements) + } yield tree).toList // persistent user-view def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil) @@ -687,8 +703,12 @@ def eq_content(other: Snapshot): Boolean = { def eq_commands(commands: (Command, Command)): Boolean = - state.command_state(version, commands._1) eq_content - other.state.command_state(other.version, commands._2) + { + val states1 = state.command_states(version, commands._1) + val states2 = other.state.command_states(other.version, commands._2) + states1.length == states2.length && + (states1 zip states2).forall({ case (st1, st2) => st1 eq_content st2 }) + } !is_outdated && !other.is_outdated && node.commands.size == other.node.commands.size && @@ -704,48 +724,39 @@ range: Text.Range, info: A, elements: Elements, - result: Command.State => (A, Text.Markup) => Option[A], + result: Command.Results => (A, Text.Markup) => Option[A], status: Boolean = false): List[Text.Info[A]] = { val former_range = revert(range) - thy_load_commands match { - case thy_load_command :: _ => - val file_name = node_name.node - val markup_index = Command.Markup_Index(status, file_name) - (for { - chunk <- thy_load_command.chunks.get(file_name).iterator - st = state.command_state(version, thy_load_command) - res = result(st) - Text.Info(r0, a) <- st.markup(markup_index).cumulate[A]( - former_range.restrict(chunk.range), info, elements, - { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) } - ).iterator - } yield Text.Info(convert(r0), a)).toList - - case _ => - val markup_index = Command.Markup_Index(status, "") - (for { - (command, command_start) <- node.command_range(former_range) - st = state.command_state(version, command) - res = result(st) - Text.Info(r0, a) <- st.markup(markup_index).cumulate[A]( - (former_range - command_start).restrict(command.range), info, elements, - { - case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) - }).iterator - } yield Text.Info(convert(r0 + command_start), a)).toList - } + val (file_name, command_range_iterator) = + thy_load_commands match { + case command :: _ => (node_name.node, Iterator((command, 0))) + case _ => ("", node.command_range(former_range)) + } + val markup_index = Command.Markup_Index(status, file_name) + (for { + (command, command_start) <- command_range_iterator + chunk <- command.chunks.get(file_name).iterator + states = state.command_states(version, command) + res = result(Command.State.merge_results(states)) + range = (former_range - command_start).restrict(chunk.range) + markup = Command.State.merge_markup(states, markup_index, range, elements) + Text.Info(r0, a) <- markup.cumulate[A](range, info, elements, + { + case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) + }).iterator + } yield Text.Info(convert(r0 + command_start), a)).toList } def select[A]( range: Text.Range, elements: Elements, - result: Command.State => Text.Markup => Option[A], + result: Command.Results => Text.Markup => Option[A], status: Boolean = false): List[Text.Info[A]] = { - def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] = + def result1(results: Command.Results): (Option[A], Text.Markup) => Option[Option[A]] = { - val res = result(st) + val res = result(results) (_: Option[A], x: Text.Markup) => res(x) match { case None => None diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/execution.ML --- a/src/Pure/PIDE/execution.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/execution.ML Thu Mar 27 21:38:45 2014 +0100 @@ -15,7 +15,10 @@ val peek: Document_ID.exec -> Future.group list val cancel: Document_ID.exec -> unit val terminate: Document_ID.exec -> unit - val fork: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future + type params = {name: string, pos: Position.T, pri: int} + val fork: params -> (unit -> 'a) -> 'a future + val print: params -> (unit -> unit) -> unit + val fork_prints: Document_ID.exec -> unit val purge: Document_ID.exec list -> unit val reset: unit -> Future.group list val shutdown: unit -> unit @@ -26,18 +29,20 @@ (* global state *) -datatype state = State of - {execution: Document_ID.execution, (*overall document execution*) - execs: Future.group list Inttab.table}; (*command execs with registered forks*) +type print = {name: string, pri: int, body: unit -> unit}; +type exec_state = Future.group list * print list; (*active forks, prints*) +type state = + Document_ID.execution * (*overall document execution*) + exec_state Inttab.table; (*running command execs*) -fun make_state (execution, execs) = State {execution = execution, execs = execs}; -fun map_state f (State {execution, execs}) = make_state (f (execution, execs)); - -val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]); +val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]); val state = Synchronized.var "Execution.state" init_state; -fun get_state () = let val State args = Synchronized.value state in args end; -fun change_state f = Synchronized.change state (map_state f); +fun get_state () = Synchronized.value state; +fun change_state_result f = Synchronized.change_result state f; +fun change_state f = Synchronized.change state f; + +fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id; (* unique running execution *) @@ -50,29 +55,30 @@ fun discontinue () = change_state (apfst (K Document_ID.none)); -fun is_running execution_id = execution_id = #execution (get_state ()); +fun is_running execution_id = execution_id = #1 (get_state ()); (* execs *) fun is_running_exec exec_id = - Inttab.defined (#execs (get_state ())) exec_id; + Inttab.defined (#2 (get_state ())) exec_id; fun running execution_id exec_id groups = - Synchronized.change_result state - (fn State {execution = execution_id', execs} => - let - val continue = execution_id = execution_id'; - val execs' = - if continue then - Inttab.update_new (exec_id, groups) execs - handle Inttab.DUP dup => - raise Fail ("Execution already registered: " ^ Document_ID.print dup) - else execs; - in (continue, make_state (execution_id', execs')) end); + change_state_result (fn (execution_id', execs) => + let + val continue = execution_id = execution_id'; + val execs' = + if continue then + Inttab.update_new (exec_id, (groups, [])) execs + handle Inttab.DUP dup => + raise Fail ("Execution already registered: " ^ Document_ID.print dup) + else execs; + in (continue, (execution_id', execs')) end); fun peek exec_id = - Inttab.lookup_list (#execs (get_state ())) exec_id; + (case Inttab.lookup (#2 (get_state ())) exec_id of + SOME (groups, _) => groups + | NONE => []); fun cancel exec_id = List.app Future.cancel_group (peek exec_id); fun terminate exec_id = List.app Future.terminate (peek exec_id); @@ -81,18 +87,24 @@ (* fork *) fun status task markups = - let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)] - in Output.status (implode (map (Markup.markup_only o props) markups)) end; + let + val props = + if ! Multithreading.trace >= 2 + then [(Markup.taskN, Task_Queue.str_of_task task)] else []; + in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end; -fun fork {name, pos, pri} e = +type params = {name: string, pos: Position.T, pri: int}; + +fun fork ({name, pos, pri}: params) e = uninterruptible (fn _ => Position.setmp_thread_data pos (fn () => let val exec_id = the_default 0 (Position.parse_id pos); val group = Future.worker_subgroup (); val _ = change_state (apsnd (fn execs => - if Inttab.defined execs exec_id - then Inttab.cons_list (exec_id, group) execs - else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id))); + (case Inttab.lookup execs exec_id of + SOME (groups, prints) => + Inttab.update (exec_id, (group :: groups, prints)) execs + | NONE => raise Fail (unregistered exec_id)))); val future = (singleton o Future.forks) @@ -112,7 +124,7 @@ status task [Markup.finished]; Output.report (Markup.markup_only Markup.bad); if exec_id = 0 then () - else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)) + else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn)) | Exn.Res _ => status task [Markup.finished]) in Exn.release result end); @@ -121,6 +133,32 @@ in future end)) (); +(* print *) + +fun print ({name, pos, pri}: params) e = + change_state (apsnd (fn execs => + let + val exec_id = the_default 0 (Position.parse_id pos); + val print = {name = name, pri = pri, body = e}; + in + (case Inttab.lookup execs exec_id of + SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs + | NONE => raise Fail (unregistered exec_id)) + end)); + +fun fork_prints exec_id = + (case Inttab.lookup (#2 (get_state ())) exec_id of + SOME (_, prints) => + if null prints orelse null (tl prints) orelse not (Multithreading.enabled ()) + then List.app (fn {body, ...} => body ()) (rev prints) + else + let val pos = Position.thread_data () in + List.app (fn {name, pri, body} => + ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints) + end + | NONE => raise Fail (unregistered exec_id)); + + (* cleanup *) fun purge exec_ids = @@ -128,7 +166,7 @@ let val execs' = fold Inttab.delete_safe exec_ids execs; val () = - (execs', ()) |-> Inttab.fold (fn (exec_id, groups) => fn () => + (execs', ()) |-> Inttab.fold (fn (exec_id, (groups, _)) => fn () => if Inttab.defined execs' exec_id then () else groups |> List.app (fn group => if Task_Queue.is_canceled group then () @@ -136,8 +174,8 @@ in execs' end); fun reset () = - Synchronized.change_result state (fn State {execs, ...} => - let val groups = Inttab.fold (append o #2) execs [] + change_state_result (fn (_, execs) => + let val groups = Inttab.fold (append o #1 o #2) execs [] in (groups, init_state) end); fun shutdown () = diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/markup_tree.scala Thu Mar 27 21:38:45 2014 +0100 @@ -20,6 +20,9 @@ val empty: Markup_Tree = new Markup_Tree(Branches.empty) + def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree = + (empty /: trees)(_.merge(_, range, elements)) + def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree = trees match { case Nil => empty @@ -113,12 +116,6 @@ private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) = this(branches + (entry.range -> entry)) - override def toString = - branches.toList.map(_._2) match { - case Nil => "Empty" - case list => list.mkString("Tree(", ",", ")") - } - private def overlapping(range: Text.Range): Branches.T = { val start = Text.Range(range.start) @@ -130,6 +127,11 @@ } } + def restrict(range: Text.Range): Markup_Tree = + new Markup_Tree(overlapping(range)) + + def is_empty: Boolean = branches.isEmpty + def + (new_markup: Text.Markup): Markup_Tree = { val new_range = new_markup.range @@ -156,44 +158,26 @@ } } - def ++ (other: Markup_Tree): Markup_Tree = - (this /: other.branches)({ case (tree, (range, entry)) => - ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) }) - - def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body = + def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree = { - def make_text(start: Text.Offset, stop: Text.Offset): XML.Body = - if (start == stop) Nil - else List(XML.Text(text.subSequence(start, stop).toString)) - - def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body = - (body /: rev_markups) { - case (b, elem) => - if (!filter(elem)) b - else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b)) - else List(XML.Wrapped_Elem(elem.markup, elem.body, b)) - } + def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree = + (tree1 /: tree2.branches)( + { case (tree, (range, entry)) => + if (!range.overlaps(root_range)) tree + else + (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))( + { case (t, elem) => t + Text.Info(range, elem) }) + }) - def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T) - : XML.Body = - { - val body = new mutable.ListBuffer[XML.Tree] - var last = elem_range.start - for ((range, entry) <- entries) { - val subrange = range.restrict(elem_range) - body ++= make_text(last, subrange.start) - body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange)) - last = subrange.stop - } - body ++= make_text(last, elem_range.stop) - make_elems(elem_markup, body.toList) + if (this eq other) this + else { + val tree1 = this.restrict(root_range) + val tree2 = other.restrict(root_range) + if (tree1.is_empty) tree2 + else merge_trees(tree1, tree2) } - make_body(root_range, Nil, overlapping(root_range)) } - def to_XML(text: CharSequence): XML.Body = - to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true) - def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements, result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] = { @@ -242,5 +226,42 @@ traverse(root_range.start, List((Text.Info(root_range, root_info), overlapping(root_range).toList))) } + + def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body = + { + def make_text(start: Text.Offset, stop: Text.Offset): XML.Body = + if (start == stop) Nil + else List(XML.Text(text.subSequence(start, stop).toString)) + + def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body = + (body /: rev_markups) { + case (b, elem) => + if (!elements(elem.name)) b + else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b)) + else List(XML.Wrapped_Elem(elem.markup, elem.body, b)) + } + + def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T) + : XML.Body = + { + val body = new mutable.ListBuffer[XML.Tree] + var last = elem_range.start + for ((range, entry) <- entries) { + val subrange = range.restrict(elem_range) + body ++= make_text(last, subrange.start) + body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange)) + last = subrange.stop + } + body ++= make_text(last, elem_range.stop) + make_elems(elem_markup, body.toList) + } + make_body(root_range, Nil, overlapping(root_range)) + } + + override def toString = + branches.toList.map(_._2) match { + case Nil => "Empty" + case list => list.mkString("Tree(", ",", ")") + } } diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/protocol.scala Thu Mar 27 21:38:45 2014 +0100 @@ -74,8 +74,11 @@ case _ => status } - def command_status(markups: List[Markup]): Status = - (Status.init /: markups)(command_status(_, _)) + def command_status(status: Status, state: Command.State): Status = + (status /: state.status)(command_status(_, _)) + + def command_status(status: Status, states: List[Command.State]): Status = + (status /: states)(command_status(_, _)) val command_status_elements = Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING, @@ -117,18 +120,19 @@ var finished = 0 var warned = 0 var failed = 0 - node.commands.foreach(command => - { - val st = state.command_state(version, command) - val status = command_status(st.status) - if (status.is_running) running += 1 - else if (status.is_finished) { - if (st.results.entries.exists(p => is_warning(p._2))) warned += 1 - else finished += 1 - } - else if (status.is_failed) failed += 1 - else unprocessed += 1 - }) + for { + command <- node.commands + states = state.command_states(version, command) + status = command_status(Status.init, states) + } { + if (status.is_running) running += 1 + else if (status.is_finished) { + val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2))) + if (warning) warned += 1 else finished += 1 + } + else if (status.is_failed) failed += 1 + else unprocessed += 1 + } Node_Status(unprocessed, running, finished, warned, failed) } @@ -149,7 +153,7 @@ var commands = Map.empty[Command, Double] for { command <- node.commands.iterator - st = state.command_state(version, command) + st <- state.command_states(version, command) command_timing = (0.0 /: st.status)({ case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds @@ -280,15 +284,14 @@ Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) def message_positions( - command_id: Document_ID.Command, - alt_id: Document_ID.Generic, + valid_id: Document_ID.Generic => Boolean, chunk: Command.Chunk, message: XML.Elem): Set[Text.Range] = { def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = props match { case Position.Reported(id, file_name, symbol_range) - if (id == command_id || id == alt_id) && file_name == chunk.file_name => + if valid_id(id) && file_name == chunk.file_name => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/query_operation.ML --- a/src/Pure/PIDE/query_operation.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/query_operation.ML Thu Mar 27 21:38:45 2014 +0100 @@ -24,7 +24,7 @@ fun status m = result (Markup.markup_only m); fun output_result s = result (Markup.markup (Markup.writelnN, []) s); fun toplevel_error exn = - result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn)); + result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn)); val _ = status Markup.running; fun run () = f {state = state, args = args, output_result = output_result}; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/query_operation.scala --- a/src/Pure/PIDE/query_operation.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/query_operation.scala Thu Mar 27 21:38:45 2014 +0100 @@ -70,20 +70,20 @@ /* snapshot */ - val (snapshot, state, removed) = + val (snapshot, command_results, removed) = current_location match { case Some(cmd) => val snapshot = editor.node_snapshot(cmd.node_name) - val state = snapshot.state.command_state(snapshot.version, cmd) + val command_results = snapshot.state.command_results(snapshot.version, cmd) val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) - (snapshot, state, removed) + (snapshot, command_results, removed) case None => - (Document.Snapshot.init, Command.empty.init_state, true) + (Document.Snapshot.init, Command.Results.empty, true) } val results = (for { - (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries + (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.entries if props.contains((Markup.INSTANCE, instance)) } yield elem).toList @@ -154,7 +154,7 @@ current_update_pending = false if (current_output != new_output && !removed) { current_output = new_output - consume_output(snapshot, state.results, new_output) + consume_output(snapshot, command_results, new_output) } if (current_status != new_status) { current_status = new_status diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/resources.ML Thu Mar 27 21:38:45 2014 +0100 @@ -211,9 +211,10 @@ val msg = "Bad file: " ^ Path.print path' ^ Position.here pos; in if strict then error msg - else - Context_Position.if_visible ctxt Output.report + else if Context_Position.is_visible ctxt then + Output.report (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg) + else () end; in path end; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/PIDE/text.scala Thu Mar 27 21:38:45 2014 +0100 @@ -45,8 +45,8 @@ def length: Int = stop - start def map(f: Offset => Offset): Range = Range(f(start), f(stop)) - def +(i: Offset): Range = map(_ + i) - def -(i: Offset): Range = map(_ - i) + def +(i: Offset): Range = if (i == 0) this else map(_ + i) + def -(i: Offset): Range = if (i == 0) this else map(_ - i) def is_singularity: Boolean = start == stop diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ROOT --- a/src/Pure/ROOT Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/ROOT Thu Mar 27 21:38:45 2014 +0100 @@ -139,6 +139,8 @@ "Isar/token.ML" "Isar/toplevel.ML" "Isar/typedecl.ML" + "ML/exn_output.ML" + "ML/exn_output_polyml.ML" "ML/exn_properties_dummy.ML" "ML/exn_properties_polyml.ML" "ML/exn_trace_polyml-5.5.1.ML" @@ -150,6 +152,7 @@ "ML/ml_env.ML" "ML/ml_lex.ML" "ML/ml_parse.ML" + "ML/ml_options.ML" "ML/ml_statistics_dummy.ML" "ML/ml_statistics_polyml-5.5.0.ML" "ML/ml_syntax.ML" diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/ROOT.ML Thu Mar 27 21:38:45 2014 +0100 @@ -69,6 +69,7 @@ use "PIDE/xml.ML"; use "PIDE/yxml.ML"; +use "PIDE/document_id.ML"; use "General/change_table.ML"; use "General/graph.ML"; @@ -193,16 +194,18 @@ (* Isar -- Intelligible Semi-Automated Reasoning *) -(*ML support*) +(*ML support and global execution*) use "ML/ml_syntax.ML"; use "ML/ml_env.ML"; +use "ML/ml_options.ML"; +use "ML/exn_output.ML"; +if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else (); +use "ML/ml_options.ML"; use "Isar/runtime.ML"; +use "PIDE/execution.ML"; use "ML/ml_compiler.ML"; if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else (); -(*global execution*) -use "PIDE/document_id.ML"; -use "PIDE/execution.ML"; use "skip_proof.ML"; use "goal.ML"; @@ -346,7 +349,7 @@ (* the Pure theory *) use "pure_syn.ML"; -Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none)); +Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none)); Context.set_thread_data NONE; structure Pure = struct val thy = Thy_Info.get_theory "Pure" end; @@ -355,7 +358,8 @@ (* ML toplevel commands *) -fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args)); +fun use_thys args = + Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args)); val use_thy = use_thys o single; val cd = File.cd o Path.explode; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 27 21:38:45 2014 +0100 @@ -417,8 +417,9 @@ report_result ctxt pos [] [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))] else if checked_len = 1 then - (if not (null ambig_msgs) andalso ambiguity_warning then - Context_Position.if_visible ctxt warning + (if not (null ambig_msgs) andalso ambiguity_warning andalso + Context_Position.is_visible ctxt then + warning (cat_lines (ambig_msgs @ ["Fortunately, only one parse tree is well-formed and type-correct,\n\ \but you may still want to disambiguate your grammar or your input."])) @@ -927,7 +928,7 @@ fun check_typs ctxt raw_tys = let val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys; - val _ = Context_Position.if_visible ctxt Output.report sorting_report; + val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else (); in tys |> apply_typ_check ctxt @@ -951,7 +952,9 @@ else I) ps tys' [] |> implode; - val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report); + val _ = + if Context_Position.is_visible ctxt then Output.report (sorting_report ^ typing_report) + else (); in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end; fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/System/command_line.ML --- a/src/Pure/System/command_line.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/System/command_line.ML Thu Mar 27 21:38:45 2014 +0100 @@ -19,7 +19,7 @@ restore_attributes body () handle exn => let val _ = - ML_Compiler.exn_error_message exn + Runtime.exn_error_message exn handle _ => Output.error_message "Exception raised, but failed to print details!"; in if Exn.is_interrupt exn then 130 else 1 end; in if rc = 0 then () else exit rc end) (); diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/System/isabelle_process.ML Thu Mar 27 21:38:45 2014 +0100 @@ -48,9 +48,9 @@ (case Symtab.lookup (Synchronized.value commands) name of NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => - (Toplevel.debugging NONE cmd args handle exn => + (Runtime.debugging NONE cmd args handle exn => error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^ - ML_Compiler.exn_message exn))); + Runtime.exn_message exn))); end; @@ -170,7 +170,7 @@ [] => (Output.error_message "Isabelle process: no input"; true) | name :: args => (task_context (fn () => run_command name args); true)) handle Runtime.TERMINATE => false - | exn => (ML_Compiler.exn_error_message exn handle crash => recover crash; true); + | exn => (Runtime.exn_error_message exn handle crash => recover crash; true); in if continue then loop channel else (Future.shutdown (); Execution.reset (); ()) diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/System/isar.ML Thu Mar 27 21:38:45 2014 +0100 @@ -97,7 +97,7 @@ | SOME (_, SOME exn_info) => (set_exn (SOME exn_info); Toplevel.setmp_thread_position tr - ML_Compiler.exn_error_message (Runtime.EXCURSION_FAIL exn_info); + Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info); true) | SOME (st', NONE) => let @@ -144,7 +144,7 @@ NONE => if secure then quit () else () | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) handle exn => - (ML_Compiler.exn_error_message exn + (Runtime.exn_error_message exn handle crash => (Synchronized.change crashes (cons crash); warning "Recovering from Isar toplevel crash -- see also Isar.crashes"); diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/Thy/thy_output.ML Thu Mar 27 21:38:45 2014 +0100 @@ -639,7 +639,7 @@ fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position) (fn {context, ...} => fn source => - (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source); + (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source); Symbol_Pos.source_content source |> #1 |> (if Config.get context quotes then quote else I) diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/config.ML --- a/src/Pure/config.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/config.ML Thu Mar 27 21:38:45 2014 +0100 @@ -131,8 +131,9 @@ print_value (get_value (Context.Theory (Context.theory_of context'))) <> print_value (get_value context') then - (Context_Position.if_visible ctxt warning - ("Ignoring local change of global option " ^ quote name); context) + (if Context_Position.is_visible ctxt then + warning ("Ignoring local change of global option " ^ quote name) + else (); context) else context' end | map_value f context = update_value f context; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/context_position.ML --- a/src/Pure/context_position.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/context_position.ML Thu Mar 27 21:38:45 2014 +0100 @@ -9,8 +9,6 @@ val is_visible_generic: Context.generic -> bool val is_visible: Proof.context -> bool val is_visible_global: theory -> bool - val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit - val if_visible_global: theory -> ('a -> unit) -> 'a -> unit val set_visible: bool -> Proof.context -> Proof.context val set_visible_global: bool -> theory -> theory val restore_visible: Proof.context -> Proof.context -> Proof.context @@ -40,9 +38,6 @@ val is_visible = is_visible_generic o Context.Proof; val is_visible_global = is_visible_generic o Context.Theory; -fun if_visible ctxt f x = if is_visible ctxt then f x else (); -fun if_visible_global thy f x = if is_visible_global thy then f x else (); - val set_visible = Context.proof_map o Data.put o SOME; val set_visible_global = Context.theory_map o Data.put o SOME; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/pure_syn.ML Thu Mar 27 21:38:45 2014 +0100 @@ -23,9 +23,10 @@ val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); val provide = Resources.provide (src_path, digest); val source = {delimited = true, text = cat_lines lines, pos = pos}; + val flags = {SML = false, redirect = true, verbose = true}; in gthy - |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) + |> ML_Context.exec (fn () => ML_Context.eval_source flags source) |> Local_Theory.propagate_ml_env |> Context.mapping provide (Local_Theory.background_theory provide) end))); diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/skip_proof.ML --- a/src/Pure/skip_proof.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/skip_proof.ML Thu Mar 27 21:38:45 2014 +0100 @@ -18,8 +18,9 @@ (* report *) fun report ctxt = - Context_Position.if_visible ctxt Output.report - (Markup.markup Markup.bad "Skipped proof"); + if Context_Position.is_visible ctxt then + Output.report (Markup.markup Markup.bad "Skipped proof") + else (); (* oracle setup *) diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Pure/unify.ML --- a/src/Pure/unify.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Pure/unify.ML Thu Mar 27 21:38:45 2014 +0100 @@ -607,8 +607,8 @@ [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq) | dp :: frigid' => if tdepth > search_bound then - (Context_Position.if_visible_global thy warning "Unification bound exceeded"; - Seq.pull reseq) + (if Context_Position.is_visible_global thy + then warning "Unification bound exceeded" else (); Seq.pull reseq) else (if tdepth > trace_bound then print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) @@ -617,7 +617,8 @@ (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq)))) end handle CANTUNIFY => - (if tdepth > trace_bound then Context_Position.if_visible_global thy tracing "Failure node" + (if tdepth > trace_bound andalso Context_Position.is_visible_global thy + then tracing "Failure node" else (); Seq.pull reseq)); val dps = map (fn (t, u) => ([], t, u)) tus; in add_unify 1 ((env, dps), Seq.empty) end; diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Tools/WWW_Find/scgi_server.ML --- a/src/Tools/WWW_Find/scgi_server.ML Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Tools/WWW_Find/scgi_server.ML Thu Mar 27 21:38:45 2014 +0100 @@ -53,7 +53,7 @@ ConditionVar.wait (thread_wait, thread_wait_mutex)); add_thread (Thread.fork (* FIXME avoid low-level Poly/ML thread primitives *) - (fn () => ML_Compiler.exn_trace threadf, + (fn () => Runtime.exn_trace threadf, [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]))) diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 27 21:38:45 2014 +0100 @@ -160,8 +160,9 @@ val root = data.root for ((command, command_start) <- snapshot.node.command_range() if !stopped) { val markup = - snapshot.state.command_state(snapshot.version, command). - markup(Command.Markup_Index.markup) + snapshot.state.command_markup( + snapshot.version, command, Command.Markup_Index.markup, + command.range, Document.Elements.full) Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) => { val range = info.range + command_start diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Mar 27 21:38:45 2014 +0100 @@ -27,7 +27,8 @@ private var zoom_factor = 100 private var do_update = true private var current_snapshot = Document.Snapshot.init - private var current_state = Command.empty.init_state + private var current_command = Command.empty + private var current_results = Command.Results.empty private var current_output: List[XML.Tree] = Nil @@ -49,33 +50,34 @@ { Swing_Thread.require() - val (new_snapshot, new_state) = + val (new_snapshot, new_command, new_results) = PIDE.editor.current_node_snapshot(view) match { case Some(snapshot) => if (follow && !snapshot.is_outdated) { PIDE.editor.current_command(view, snapshot) match { case Some(cmd) => - (snapshot, snapshot.state.command_state(snapshot.version, cmd)) + (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd)) case None => - (Document.Snapshot.init, Command.empty.init_state) + (Document.Snapshot.init, Command.empty, Command.Results.empty) } } - else (current_snapshot, current_state) - case None => (current_snapshot, current_state) + else (current_snapshot, current_command, current_results) + case None => (current_snapshot, current_command, current_results) } val new_output = - if (!restriction.isDefined || restriction.get.contains(new_state.command)) { + if (!restriction.isDefined || restriction.get.contains(new_command)) { val rendering = Rendering(new_snapshot, PIDE.options.value) - rendering.output_messages(new_state) + rendering.output_messages(new_results) } else current_output if (new_output != current_output) - pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output)) + pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output)) current_snapshot = new_snapshot - current_state = new_state + current_command = new_command + current_results = new_results current_output = new_output } @@ -149,8 +151,7 @@ tooltip = "Detach window with static copy of current output" reactions += { case ButtonClicked(_) => - Info_Dockable(view, current_snapshot, - current_state.results, Pretty.separate(current_output)) + Info_Dockable(view, current_snapshot, current_results, Pretty.separate(current_output)) } } diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Tools/jEdit/src/rendering.scala Thu Mar 27 21:38:45 2014 +0100 @@ -380,13 +380,13 @@ /* active elements */ def active(range: Text.Range): Option[Text.Info[XML.Elem]] = - snapshot.select(range, Rendering.active_elements, command_state => + snapshot.select(range, Rendering.active_elements, command_results => { case Text.Info(info_range, elem) => if (elem.name == Markup.DIALOG) { elem match { case Protocol.Dialog(_, serial, _) - if !command_state.results.defined(serial) => + if !command_results.defined(serial) => Some(Text.Info(snapshot.convert(info_range), elem)) case _ => None } @@ -397,8 +397,8 @@ def command_results(range: Text.Range): Command.Results = { val results = - snapshot.select[Command.Results](range, Document.Elements.full, command_state => - { case _ => Some(command_state.results) }).map(_.info) + snapshot.select[Command.Results](range, Document.Elements.full, command_results => + { case _ => Some(command_results) }).map(_.info) (Command.Results.empty /: results)(_ ++ _) } @@ -592,8 +592,8 @@ message_colors.get(pri).map((_, is_separator)) } - def output_messages(st: Command.State): List[XML.Tree] = - st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList + def output_messages(results: Command.Results): List[XML.Tree] = + results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList /* text background */ @@ -606,7 +606,7 @@ Text.Info(r, result) <- snapshot.cumulate[(Option[Protocol.Status], Option[Color])]( range, (Some(Protocol.Status.init), None), Rendering.background_elements, - command_state => + command_results => { case (((Some(status), color), Text.Info(_, XML.Elem(markup, _)))) if (Protocol.command_status_elements(markup.name)) => @@ -616,7 +616,7 @@ case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => Some((None, Some(intensify_color))) case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => - command_state.results.get(serial) match { + command_results.get(serial) match { case Some(Protocol.Dialog_Result(res)) if res == result => Some((None, Some(active_result_color))) case _ => diff -r 801a72ad52d3 -r 4d8955cdfb97 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Mar 26 11:05:25 2014 -0700 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Mar 27 21:38:45 2014 +0100 @@ -26,7 +26,8 @@ /* component state -- owned by Swing thread */ private var current_snapshot = Document.State.init.snapshot() - private var current_state = Command.empty.init_state + private var current_command = Command.empty + private var current_results = Command.Results.empty private var current_id = 0L private var do_update = true private var do_auto_reply = false @@ -77,7 +78,7 @@ private def show_trace() { - val trace = Simplifier_Trace.generate_trace(current_state.results) + val trace = Simplifier_Trace.generate_trace(current_results) new Simplifier_Trace_Window(view, current_snapshot, trace) } @@ -92,7 +93,7 @@ { set_context( current_snapshot, - Simplifier_Trace.handle_results(PIDE.session, current_id, current_state.results) + Simplifier_Trace.handle_results(PIDE.session, current_id, current_results) ) } @@ -103,23 +104,24 @@ private def handle_update(follow: Boolean) { - val (new_snapshot, new_state, new_id) = + val (new_snapshot, new_command, new_results, new_id) = PIDE.editor.current_node_snapshot(view) match { case Some(snapshot) => if (follow && !snapshot.is_outdated) { PIDE.editor.current_command(view, snapshot) match { case Some(cmd) => - (snapshot, snapshot.state.command_state(snapshot.version, cmd), cmd.id) + (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id) case None => - (Document.State.init.snapshot(), Command.empty.init_state, 0L) + (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L) } } - else (current_snapshot, current_state, current_id) - case None => (current_snapshot, current_state, current_id) + else (current_snapshot, current_command, current_results, current_id) + case None => (current_snapshot, current_command, current_results, current_id) } current_snapshot = new_snapshot - current_state = new_state + current_command = new_command + current_results = new_results current_id = new_id update_contents() }