clarified protocol: support "isabelle log" on failed theories as well;

--- a/src/Pure/PIDE/document.scala	Wed Dec 09 20:33:02 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Dec 09 22:07:14 2020 +0100
@@ -988,16 +988,16 @@
       }
     }
 
-    def end_theory(theory: String): (Snapshot, State) =
-      theories.collectFirst({ case (_, st) if st.command.node_name.theory == theory => st }) match {
+    def end_theory(id: Document_ID.Exec): (Snapshot, State) =
+      theories.get(id) match {
         case None => fail
         case Some(st) =>
           val command = st.command
           val node_name = command.node_name
           val command1 =
-            Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name,
+            Command.unparsed(command.source, theory = true, id = id, node_name = node_name,
               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
-          val state1 = copy(theories = theories - command1.id)
+          val state1 = copy(theories = theories - id)
           val snapshot = state1.command_snippet(command1)
           (snapshot, state1)
       }

--- a/src/Pure/PIDE/markup.ML	Wed Dec 09 20:33:02 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Dec 09 22:07:14 2020 +0100
@@ -222,7 +222,6 @@
   val theory_timing: Properties.entry
   val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
-  val finished_theory: string -> Properties.T
   val build_session_finished: Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
@@ -698,7 +697,6 @@
 val session_timing = (functionN, "session_timing");
 
 fun loading_theory name = [("function", "loading_theory"), (nameN, name)];
-fun finished_theory name = [("function", "finished_theory"), (nameN, name)];
 
 val build_session_finished = [("function", "build_session_finished")];
 

--- a/src/Pure/PIDE/markup.scala	Wed Dec 09 20:33:02 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Dec 09 22:07:14 2020 +0100
@@ -612,7 +612,6 @@
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Properties_Function("loading_theory")
-  object Finished_Theory extends Name_Function("finished_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
   object Commands_Accepted extends Function("commands_accepted")

--- a/src/Pure/PIDE/session.scala	Wed Dec 09 20:33:02 2020 +0100
+++ b/src/Pure/PIDE/session.scala	Wed Dec 09 22:07:14 2020 +0100
@@ -513,13 +513,6 @@
                 try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) }
                 catch { case _: Document.State.Fail => bad_output() }
 
-              case Markup.Finished_Theory(theory) =>
-                try {
-                  val snapshot = global_state.change_result(_.end_theory(theory))
-                  finished_theories.post(snapshot)
-                }
-                catch { case _: Document.State.Fail => bad_output() }
-
               case List(Markup.Commands_Accepted.PROPERTY) =>
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
@@ -584,6 +577,10 @@
 
             case Markup.Process_Result(result) if output.is_exit =>
               if (prover.defined) protocol_handlers.exit()
+              for (id <- global_state.value.theories.keys) {
+                val snapshot = global_state.change_result(_.end_theory(id))
+                finished_theories.post(snapshot)
+              }
               file_formats.stop_session
               phase = Session.Terminated(result)
               prover.reset

--- a/src/Pure/Thy/thy_info.ML	Wed Dec 09 20:33:02 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Dec 09 22:07:14 2020 +0100
@@ -56,8 +56,7 @@
 );
 
 fun apply_presentation (context: presentation_context) thy =
- (ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
-  Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) []);
+  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));