# HG changeset patch
# User wenzelm
# Date 1421326886 -3600
# Node ID b13ff987c5597abc63aa06671b5730a98883538e
# Parent  7090199d3f788966028f265cf0f45a09740b71ff
refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;

diff -r 7090199d3f78 -r b13ff987c559 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Jan 15 12:54:08 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Jan 15 14:01:26 2015 +0100
@@ -53,45 +53,46 @@
 
 val _ =
   Isabelle_Process.protocol_command "Document.update"
-    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
-      let
-        val _ = Execution.discontinue ();
+    (Future.task_context "Document.update" (Future.new_group NONE)
+      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
+        let
+          val _ = Execution.discontinue ();
 
-        val old_id = Document_ID.parse old_id_string;
-        val new_id = Document_ID.parse new_id_string;
-        val edits =
-          YXML.parse_body edits_yxml |>
-            let open XML.Decode in
-              list (pair string
-                (variant
-                 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
-                  fn ([], a) =>
-                    let
-                      val (master, (name, (imports, (keywords, errors)))) =
-                        pair string (pair string (pair (list string)
-                          (pair (list (pair string
-                            (option (pair (pair string (list string)) (list string)))))
-                            (list string)))) a;
-                      val imports' = map (rpair Position.none) imports;
-                      val header = Thy_Header.make (name, Position.none) imports' keywords;
-                    in Document.Deps (master, header, errors) end,
-                  fn (a :: b, c) =>
-                    Document.Perspective (bool_atom a, map int_atom b,
-                      list (pair int (pair string (list string))) c)]))
-            end;
+          val old_id = Document_ID.parse old_id_string;
+          val new_id = Document_ID.parse new_id_string;
+          val edits =
+            YXML.parse_body edits_yxml |>
+              let open XML.Decode in
+                list (pair string
+                  (variant
+                   [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+                    fn ([], a) =>
+                      let
+                        val (master, (name, (imports, (keywords, errors)))) =
+                          pair string (pair string (pair (list string)
+                            (pair (list (pair string
+                              (option (pair (pair string (list string)) (list string)))))
+                              (list string)))) a;
+                        val imports' = map (rpair Position.none) imports;
+                        val header = Thy_Header.make (name, Position.none) imports' keywords;
+                      in Document.Deps (master, header, errors) end,
+                    fn (a :: b, c) =>
+                      Document.Perspective (bool_atom a, map int_atom b,
+                        list (pair int (pair string (list string))) c)]))
+              end;
 
-        val (removed, assign_update, state') = Document.update old_id new_id edits state;
-        val _ = List.app Execution.terminate removed;
-        val _ = Execution.purge removed;
-        val _ = List.app Isabelle_Process.reset_tracing removed;
+          val (removed, assign_update, state') = Document.update old_id new_id edits state;
+          val _ = List.app Execution.terminate removed;
+          val _ = Execution.purge removed;
+          val _ = List.app Isabelle_Process.reset_tracing removed;
 
-        val _ =
-          Output.protocol_message Markup.assign_update
-            [(new_id, assign_update) |>
-              let open XML.Encode
-              in pair int (list (pair int (list int))) end
-              |> YXML.string_of_body];
-      in Document.start_execution state' end));
+          val _ =
+            Output.protocol_message Markup.assign_update
+              [(new_id, assign_update) |>
+                let open XML.Encode
+                in pair int (list (pair int (list int))) end
+                |> YXML.string_of_body];
+        in Document.start_execution state' end)));
 
 val _ =
   Isabelle_Process.protocol_command "Document.remove_versions"
diff -r 7090199d3f78 -r b13ff987c559 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Jan 15 12:54:08 2015 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Jan 15 14:01:26 2015 +0100
@@ -162,9 +162,6 @@
   System_Channel.input_line channel
   |> Option.map (fn line => map (read_chunk channel) (space_explode "," line));
 
-fun task_context e =
-  Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
-
 in
 
 fun loop channel =
@@ -173,7 +170,7 @@
       (case read_command channel of
         NONE => false
       | SOME [] => (Output.system_message "Isabelle process: no input"; true)
-      | SOME (name :: args) => (task_context (fn () => run_command name args); true))
+      | SOME (name :: args) => (run_command name args; true))
       handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
   in
     if continue then loop channel