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 **)