# HG changeset patch # User wenzelm # Date 1417013072 -3600 # Node ID cbe9563c03d1d5d00493c489df51809d8d0dd43d # Parent 5a7157b8e870d7caa699703ec74929b14eeb71f4 even more exception traces for Document.update, which goes through additional execution wrappers; diff -r 5a7157b8e870 -r cbe9563c03d1 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Wed Nov 26 14:35:55 2014 +0100 +++ b/src/Pure/Isar/runtime.ML Wed Nov 26 15:44:32 2014 +0100 @@ -17,6 +17,7 @@ val exn_error_message: exn -> unit val exn_system_message: exn -> unit val exn_trace: (unit -> 'a) -> 'a + val exn_trace_system: (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 @@ -134,6 +135,7 @@ val exn_error_message = Output.error_message o exn_message; val exn_system_message = Output.system_message o exn_message; fun exn_trace e = print_exception_trace exn_message tracing e; +fun exn_trace_system e = print_exception_trace exn_message Output.system_message e; diff -r 5a7157b8e870 -r cbe9563c03d1 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Nov 26 14:35:55 2014 +0100 +++ b/src/Pure/PIDE/document.ML Wed Nov 26 15:44:32 2014 +0100 @@ -559,7 +559,7 @@ in -fun update old_version_id new_version_id edits state = +fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () => let val old_version = the_version state old_version_id; val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); @@ -575,61 +575,63 @@ (singleton o Future.forks) {name = "Document.update", group = NONE, deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} - (fn () => timeit ("Document.update " ^ name) (fn () => - let - val keywords = get_keywords (); - val imports = map (apsnd Future.join) deps; - val imports_result_changed = exists (#4 o #1 o #2) imports; - val node_required = Symtab.defined required name; - in - if Symtab.defined edited name orelse visible_node node orelse - imports_result_changed orelse Symtab.defined required0 name <> node_required - then + (fn () => + timeit ("Document.update " ^ name) (fn () => + Runtime.exn_trace_system (fn () => let - val node0 = node_of old_version name; - val init = init_theory imports node; - val proper_init = - check_theory false name node andalso - forall (fn (name, (_, node)) => check_theory true name node) imports; + val keywords = get_keywords (); + val imports = map (apsnd Future.join) deps; + val imports_result_changed = exists (#4 o #1 o #2) imports; + val node_required = Symtab.defined required name; + in + if Symtab.defined edited name orelse visible_node node orelse + imports_result_changed orelse Symtab.defined required0 name <> node_required + then + let + val node0 = node_of old_version name; + val init = init_theory imports node; + val proper_init = + check_theory false name node andalso + forall (fn (name, (_, node)) => check_theory true name node) imports; - val (print_execs, common, (still_visible, initial)) = - if imports_result_changed then (assign_update_empty, NONE, (true, true)) - else last_common keywords state node_required node0 node; - val common_command_exec = the_default_entry node common; + val (print_execs, common, (still_visible, initial)) = + if imports_result_changed then (assign_update_empty, NONE, (true, true)) + else last_common keywords state node_required node0 node; + val common_command_exec = the_default_entry node common; - val (updated_execs, (command_id', (eval', _)), _) = - (print_execs, common_command_exec, if initial then SOME init else NONE) - |> (still_visible orelse node_required) ? - iterate_entries_after common - (fn ((prev, id), _) => fn res => - if not node_required andalso prev = visible_last node then NONE - else new_exec keywords state node proper_init id res) node; + val (updated_execs, (command_id', (eval', _)), _) = + (print_execs, common_command_exec, if initial then SOME init else NONE) + |> (still_visible orelse node_required) ? + iterate_entries_after common + (fn ((prev, id), _) => fn res => + if not node_required andalso prev = visible_last node then NONE + else new_exec keywords state node proper_init id res) node; - val assigned_execs = - (node0, updated_execs) |-> iterate_entries_after common - (fn ((_, command_id0), exec0) => fn res => - if is_none exec0 then NONE - else if assign_update_defined updated_execs command_id0 then SOME res - else SOME (assign_update_new (command_id0, NONE) res)); + val assigned_execs = + (node0, updated_execs) |-> iterate_entries_after common + (fn ((_, command_id0), exec0) => fn res => + if is_none exec0 then NONE + else if assign_update_defined updated_execs command_id0 then SOME res + else SOME (assign_update_new (command_id0, NONE) res)); - val last_exec = - if command_id' = Document_ID.none then NONE else SOME command_id'; - val result = - if is_none last_exec orelse is_some (after_entry node last_exec) then NONE - else SOME eval'; + val last_exec = + if command_id' = Document_ID.none then NONE else SOME command_id'; + val result = + if is_none last_exec orelse is_some (after_entry node last_exec) then NONE + else SOME eval'; - val assign_update = assign_update_result assigned_execs; - val removed = maps (removed_execs node0) assign_update; - val _ = List.app Execution.cancel removed; + val assign_update = assign_update_result assigned_execs; + val removed = maps (removed_execs node0) assign_update; + val _ = List.app Execution.cancel removed; - val node' = node - |> assign_update_apply assigned_execs - |> set_result result; - val assigned_node = SOME (name, node'); - val result_changed = changed_result node0 node'; - in ((removed, assign_update, assigned_node, result_changed), node') end - else (([], [], NONE, false), node) - end))) + val node' = node + |> assign_update_apply assigned_execs + |> set_result result; + val assigned_node = SOME (name, node'); + val result_changed = changed_result node0 node'; + in ((removed, assign_update, assigned_node, result_changed), node') end + else (([], [], NONE, false), node) + end)))) |> Future.joins |> map #1); val removed = maps #1 updated; @@ -639,7 +641,7 @@ val state' = state |> define_version new_version_id (fold put_node assigned_nodes new_version); - in (removed, assign_update, state') end; + in (removed, assign_update, state') end); end; diff -r 5a7157b8e870 -r cbe9563c03d1 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Nov 26 14:35:55 2014 +0100 +++ b/src/Pure/System/isabelle_process.ML Wed Nov 26 15:44:32 2014 +0100 @@ -47,7 +47,7 @@ (case Symtab.lookup (Synchronized.value commands) name of NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => - (print_exception_trace Runtime.exn_message Output.system_message (fn () => cmd args) + (Runtime.exn_trace_system (fn () => cmd args) handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name))); end;