check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);

--- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 24 11:32:12 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 24 12:35:39 2012 +0200
@@ -530,15 +530,11 @@
 
 (* markup commands *)
 
-fun check_text (txt, pos) state =
- (Position.report pos Isabelle_Markup.doc_source;
-  ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
-
 fun header_markup txt = Toplevel.keep (fn state =>
-  if Toplevel.is_toplevel state then check_text txt state
+  if Toplevel.is_toplevel state then Thy_Output.check_text txt state
   else raise Toplevel.UNDEF);
 
-fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt);
-val proof_markup = Toplevel.present_proof o check_text;
+fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt);
+val proof_markup = Toplevel.present_proof o Thy_Output.check_text;
 
 end;

--- a/src/Pure/Isar/outer_syntax.ML	Fri Aug 24 11:32:12 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Aug 24 12:35:39 2012 +0200
@@ -33,6 +33,7 @@
   val parse: Position.T -> string -> Toplevel.transition list
   type isar
   val isar: TextIO.instream -> bool -> isar
+  val span_cmts: Token.T list -> Token.T list
   val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
@@ -267,6 +268,22 @@
   |> toplevel_source term (SOME true) lookup_commands_dynamic;
 
 
+(* side-comments *)
+
+local
+
+fun cmts (t1 :: t2 :: toks) =
+      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
+      else cmts (t2 :: toks)
+  | cmts toks = [];
+
+in
+
+val span_cmts = filter Token.is_proper #> cmts;
+
+end;
+
+
 (* read toplevel commands -- fail-safe *)
 
 fun read_span outer_syntax toks =

--- 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;

--- a/src/Pure/PIDE/document.ML	Fri Aug 24 11:32:12 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 24 12:35:39 2012 +0200
@@ -442,15 +442,19 @@
         else (I, init);
       val exec_id' = new_id ();
       val exec_id'_string = print_id exec_id';
-      val tr =
+      val cmd =
         Position.setmp_thread_data (Position.id_only exec_id'_string)
           (fn () =>
-            #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
-            |> modify_init
-            |> Toplevel.put_id exec_id'_string);
+            let
+              val tr =
+                #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
+                |> modify_init
+                |> Toplevel.put_id exec_id'_string;
+              val cmts = Outer_Syntax.span_cmts span;
+            in (tr, cmts) end);
       val exec' =
         Command.memo (fn () =>
-          Command.run_command (tr ()) (fst (Command.memo_result (snd (snd command_exec)))));
+          Command.run_command (cmd ()) (fst (Command.memo_result (snd (snd command_exec)))));
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;
 

--- a/src/Pure/Thy/thy_output.ML	Fri Aug 24 11:32:12 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Aug 24 12:35:39 2012 +0200
@@ -32,6 +32,7 @@
   val modes: string list Unsynchronized.ref
   val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
+  val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   val pretty_text: Proof.context -> string -> Pretty.T
@@ -202,6 +203,11 @@
   end;
 
 
+fun check_text (txt, pos) state =
+ (Position.report pos Isabelle_Markup.doc_source;
+  ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
+
+
 
 (** present theory source **)