merged

--- a/src/Pure/Admin/build_history.scala	Thu Oct 27 15:51:54 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Oct 27 21:52:44 2016 +0200
@@ -379,7 +379,7 @@
     progress: Progress = Ignore_Progress,
     progress_result: (String, Bytes) => Unit = (log_name: String, bytes: Bytes) => (),
     options: String = "",
-    args: String = ""): List[(String, Bytes)] =
+    args: String = ""): (List[(String, Bytes)], Process_Result) =
   {
     val isabelle_admin = isabelle_repos_self + Path.explode("Admin")
 
@@ -428,12 +428,13 @@
       result += res
     }
 
-    ssh.execute(
-      ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
-        ssh.bash_path(isabelle_repos_other) + " " + args,
-      progress_stdout = progress_stdout _,
-      progress_stderr = progress.echo(_)).check
+    val process_result =
+      ssh.execute(
+        ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
+          ssh.bash_path(isabelle_repos_other) + " " + args,
+        progress_stdout = progress_stdout _,
+        progress_stderr = progress.echo(_))
 
-    result.toList
+    (result.toList, process_result)
   }
 }

--- a/src/Pure/Isar/proof.ML	Thu Oct 27 15:51:54 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Oct 27 21:52:44 2016 +0200
@@ -1163,9 +1163,18 @@
 
 local
 
-fun terminal_proof qeds initial terminal =
-  proof (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
-  #> Seq.the_result "";
+fun terminal_proof qeds initial terminal state =
+  let
+    val ctxt = context_of state;
+    val check_closure = Method.check_text ctxt #> Method.map_source (Method.method_closure ctxt);
+    val initial' = apfst check_closure initial;
+    val terminal' = (apfst o Option.map o apfst) check_closure terminal;
+  in
+    state
+    |> proof (SOME initial')
+    |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
+    |> Seq.the_result ""
+  end;
 
 in
 

--- a/src/Pure/Isar/token.ML	Thu Oct 27 15:51:54 2016 +0200
+++ b/src/Pure/Isar/token.ML	Thu Oct 27 21:52:44 2016 +0200
@@ -507,8 +507,9 @@
       SOME {name, ...} => (src, Name_Space.get table name)
     | NONE =>
         let
-          val (name, x) =
-            Name_Space.check (Context.Proof ctxt) table (content_of head, pos_of head);
+          val pos = pos_of head;
+          val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos);
+          val _ = Context_Position.report ctxt pos Markup.operator;
           val kind = Name_Space.kind_of (Name_Space.space_of_table table);
           fun print ctxt' =
             Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name;
@@ -720,11 +721,15 @@
 fun syntax_generic scan src context =
   let
     val (name, pos) = name_of_src src;
+    val old_reports = maps reports_of_value src;
     val args1 = map init_assignable (args_of_src src);
     fun reported_text () =
       if Context_Position.is_visible_generic context then
-        ((pos, Markup.operator) :: maps (reports_of_value o closure) args1)
-        |> map (fn (p, m) => Position.reported_text p m "")
+        let val new_reports = maps (reports_of_value o closure) args1 in
+          if old_reports <> new_reports then
+            map (fn (p, m) => Position.reported_text p m "") new_reports
+          else []
+        end
       else [];
   in
     (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of