src/Pure/PIDE/command.ML
changeset 48918 6e5fd4585512
parent 48772 e46cd0d26481
child 49036 4680c4046814
--- a/src/Pure/PIDE/command.ML	Fri Aug 24 11:32:12 2012 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Aug 24 12:35:39 2012 +0200
@@ -13,7 +13,7 @@
   val memo_value: 'a -> 'a memo
   val memo_eval: 'a memo -> 'a
   val memo_result: 'a memo -> 'a
-  val run_command: Toplevel.transition ->
+  val run_command: Toplevel.transition * Token.T list ->
     Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
 end;
 
@@ -73,6 +73,13 @@
   | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
   | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
 
+fun check_cmts tr cmts st =
+  Toplevel.setmp_thread_position tr
+    (fn () => cmts
+      |> maps (fn cmt =>
+        (Thy_Output.check_text (Token.source_position_of cmt) st; [])
+          handle exn => ML_Compiler.exn_messages exn)) ();
+
 fun timing tr t =
   if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
 
@@ -89,7 +96,7 @@
 
 in
 
-fun run_command tr (st, malformed) =
+fun run_command (tr, cmts) (st, malformed) =
   if malformed then ((Toplevel.toplevel, malformed), no_print)
   else
     let
@@ -100,7 +107,9 @@
       val _ = Multithreading.interrupted ();
       val _ = Toplevel.status tr Isabelle_Markup.forked;
       val start = Timing.start ();
-      val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+      val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+      val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
+      val errs = errs1 @ errs2;
       val _ = timing tr (Timing.result start);
       val _ = Toplevel.status tr Isabelle_Markup.joined;
       val _ = List.app (Toplevel.error_msg tr) errs;