even more exception traces for Document.update, which goes through additional execution wrappers;
authorwenzelm
Wed Nov 26 15:44:32 2014 +0100 (2014-11-26 ago)
changeset 59056cbe9563c03d1
parent 59055 5a7157b8e870
child 59057 5b649fb2f2e1
even more exception traces for Document.update, which goes through additional execution wrappers;
src/Pure/Isar/runtime.ML
src/Pure/PIDE/document.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/Isar/runtime.ML	Wed Nov 26 14:35:55 2014 +0100
     1.2 +++ b/src/Pure/Isar/runtime.ML	Wed Nov 26 15:44:32 2014 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4    val exn_error_message: exn -> unit
     1.5    val exn_system_message: exn -> unit
     1.6    val exn_trace: (unit -> 'a) -> 'a
     1.7 +  val exn_trace_system: (unit -> 'a) -> 'a
     1.8    val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
     1.9    val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    1.10    val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
    1.11 @@ -134,6 +135,7 @@
    1.12  val exn_error_message = Output.error_message o exn_message;
    1.13  val exn_system_message = Output.system_message o exn_message;
    1.14  fun exn_trace e = print_exception_trace exn_message tracing e;
    1.15 +fun exn_trace_system e = print_exception_trace exn_message Output.system_message e;
    1.16  
    1.17  
    1.18  
     2.1 --- a/src/Pure/PIDE/document.ML	Wed Nov 26 14:35:55 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.ML	Wed Nov 26 15:44:32 2014 +0100
     2.3 @@ -559,7 +559,7 @@
     2.4  
     2.5  in
     2.6  
     2.7 -fun update old_version_id new_version_id edits state =
     2.8 +fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () =>
     2.9    let
    2.10      val old_version = the_version state old_version_id;
    2.11      val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
    2.12 @@ -575,61 +575,63 @@
    2.13            (singleton o Future.forks)
    2.14              {name = "Document.update", group = NONE,
    2.15                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
    2.16 -            (fn () => timeit ("Document.update " ^ name) (fn () =>
    2.17 -              let
    2.18 -                val keywords = get_keywords ();
    2.19 -                val imports = map (apsnd Future.join) deps;
    2.20 -                val imports_result_changed = exists (#4 o #1 o #2) imports;
    2.21 -                val node_required = Symtab.defined required name;
    2.22 -              in
    2.23 -                if Symtab.defined edited name orelse visible_node node orelse
    2.24 -                  imports_result_changed orelse Symtab.defined required0 name <> node_required
    2.25 -                then
    2.26 +            (fn () =>
    2.27 +              timeit ("Document.update " ^ name) (fn () =>
    2.28 +                Runtime.exn_trace_system (fn () =>
    2.29                    let
    2.30 -                    val node0 = node_of old_version name;
    2.31 -                    val init = init_theory imports node;
    2.32 -                    val proper_init =
    2.33 -                      check_theory false name node andalso
    2.34 -                      forall (fn (name, (_, node)) => check_theory true name node) imports;
    2.35 +                    val keywords = get_keywords ();
    2.36 +                    val imports = map (apsnd Future.join) deps;
    2.37 +                    val imports_result_changed = exists (#4 o #1 o #2) imports;
    2.38 +                    val node_required = Symtab.defined required name;
    2.39 +                  in
    2.40 +                    if Symtab.defined edited name orelse visible_node node orelse
    2.41 +                      imports_result_changed orelse Symtab.defined required0 name <> node_required
    2.42 +                    then
    2.43 +                      let
    2.44 +                        val node0 = node_of old_version name;
    2.45 +                        val init = init_theory imports node;
    2.46 +                        val proper_init =
    2.47 +                          check_theory false name node andalso
    2.48 +                          forall (fn (name, (_, node)) => check_theory true name node) imports;
    2.49  
    2.50 -                    val (print_execs, common, (still_visible, initial)) =
    2.51 -                      if imports_result_changed then (assign_update_empty, NONE, (true, true))
    2.52 -                      else last_common keywords state node_required node0 node;
    2.53 -                    val common_command_exec = the_default_entry node common;
    2.54 +                        val (print_execs, common, (still_visible, initial)) =
    2.55 +                          if imports_result_changed then (assign_update_empty, NONE, (true, true))
    2.56 +                          else last_common keywords state node_required node0 node;
    2.57 +                        val common_command_exec = the_default_entry node common;
    2.58  
    2.59 -                    val (updated_execs, (command_id', (eval', _)), _) =
    2.60 -                      (print_execs, common_command_exec, if initial then SOME init else NONE)
    2.61 -                      |> (still_visible orelse node_required) ?
    2.62 -                        iterate_entries_after common
    2.63 -                          (fn ((prev, id), _) => fn res =>
    2.64 -                            if not node_required andalso prev = visible_last node then NONE
    2.65 -                            else new_exec keywords state node proper_init id res) node;
    2.66 +                        val (updated_execs, (command_id', (eval', _)), _) =
    2.67 +                          (print_execs, common_command_exec, if initial then SOME init else NONE)
    2.68 +                          |> (still_visible orelse node_required) ?
    2.69 +                            iterate_entries_after common
    2.70 +                              (fn ((prev, id), _) => fn res =>
    2.71 +                                if not node_required andalso prev = visible_last node then NONE
    2.72 +                                else new_exec keywords state node proper_init id res) node;
    2.73  
    2.74 -                    val assigned_execs =
    2.75 -                      (node0, updated_execs) |-> iterate_entries_after common
    2.76 -                        (fn ((_, command_id0), exec0) => fn res =>
    2.77 -                          if is_none exec0 then NONE
    2.78 -                          else if assign_update_defined updated_execs command_id0 then SOME res
    2.79 -                          else SOME (assign_update_new (command_id0, NONE) res));
    2.80 +                        val assigned_execs =
    2.81 +                          (node0, updated_execs) |-> iterate_entries_after common
    2.82 +                            (fn ((_, command_id0), exec0) => fn res =>
    2.83 +                              if is_none exec0 then NONE
    2.84 +                              else if assign_update_defined updated_execs command_id0 then SOME res
    2.85 +                              else SOME (assign_update_new (command_id0, NONE) res));
    2.86  
    2.87 -                    val last_exec =
    2.88 -                      if command_id' = Document_ID.none then NONE else SOME command_id';
    2.89 -                    val result =
    2.90 -                      if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
    2.91 -                      else SOME eval';
    2.92 +                        val last_exec =
    2.93 +                          if command_id' = Document_ID.none then NONE else SOME command_id';
    2.94 +                        val result =
    2.95 +                          if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
    2.96 +                          else SOME eval';
    2.97  
    2.98 -                    val assign_update = assign_update_result assigned_execs;
    2.99 -                    val removed = maps (removed_execs node0) assign_update;
   2.100 -                    val _ = List.app Execution.cancel removed;
   2.101 +                        val assign_update = assign_update_result assigned_execs;
   2.102 +                        val removed = maps (removed_execs node0) assign_update;
   2.103 +                        val _ = List.app Execution.cancel removed;
   2.104  
   2.105 -                    val node' = node
   2.106 -                      |> assign_update_apply assigned_execs
   2.107 -                      |> set_result result;
   2.108 -                    val assigned_node = SOME (name, node');
   2.109 -                    val result_changed = changed_result node0 node';
   2.110 -                  in ((removed, assign_update, assigned_node, result_changed), node') end
   2.111 -                else (([], [], NONE, false), node)
   2.112 -              end)))
   2.113 +                        val node' = node
   2.114 +                          |> assign_update_apply assigned_execs
   2.115 +                          |> set_result result;
   2.116 +                        val assigned_node = SOME (name, node');
   2.117 +                        val result_changed = changed_result node0 node';
   2.118 +                      in ((removed, assign_update, assigned_node, result_changed), node') end
   2.119 +                    else (([], [], NONE, false), node)
   2.120 +                  end))))
   2.121        |> Future.joins |> map #1);
   2.122  
   2.123      val removed = maps #1 updated;
   2.124 @@ -639,7 +641,7 @@
   2.125      val state' = state
   2.126        |> define_version new_version_id (fold put_node assigned_nodes new_version);
   2.127  
   2.128 -  in (removed, assign_update, state') end;
   2.129 +  in (removed, assign_update, state') end);
   2.130  
   2.131  end;
   2.132  
     3.1 --- a/src/Pure/System/isabelle_process.ML	Wed Nov 26 14:35:55 2014 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Nov 26 15:44:32 2014 +0100
     3.3 @@ -47,7 +47,7 @@
     3.4    (case Symtab.lookup (Synchronized.value commands) name of
     3.5      NONE => error ("Undefined Isabelle protocol command " ^ quote name)
     3.6    | SOME cmd =>
     3.7 -      (print_exception_trace Runtime.exn_message Output.system_message (fn () => cmd args)
     3.8 +      (Runtime.exn_trace_system (fn () => cmd args)
     3.9          handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name)));
    3.10  
    3.11  end;