# HG changeset patch # User wenzelm # Date 1345804539 -7200 # Node ID 6e5fd4585512c3103ffc044e7d7f7ac91951c4df # Parent ce37d4f8b4f487bdb4de4899fa6a89d7b861cedd check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source); diff -r ce37d4f8b4f4 -r 6e5fd4585512 src/Pure/Isar/isar_cmd.ML --- 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; diff -r ce37d4f8b4f4 -r 6e5fd4585512 src/Pure/Isar/outer_syntax.ML --- 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 = diff -r ce37d4f8b4f4 -r 6e5fd4585512 src/Pure/PIDE/command.ML --- 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; diff -r ce37d4f8b4f4 -r 6e5fd4585512 src/Pure/PIDE/document.ML --- 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; diff -r ce37d4f8b4f4 -r 6e5fd4585512 src/Pure/Thy/thy_output.ML --- 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 **)