check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
authorwenzelm
Fri Aug 24 12:35:39 2012 +0200 (2012-08-24 ago)
changeset 489186e5fd4585512
parent 48917 ce37d4f8b4f4
child 48919 aaca64a7390c
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 24 11:32:12 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 24 12:35:39 2012 +0200
     1.3 @@ -530,15 +530,11 @@
     1.4  
     1.5  (* markup commands *)
     1.6  
     1.7 -fun check_text (txt, pos) state =
     1.8 - (Position.report pos Isabelle_Markup.doc_source;
     1.9 -  ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
    1.10 -
    1.11  fun header_markup txt = Toplevel.keep (fn state =>
    1.12 -  if Toplevel.is_toplevel state then check_text txt state
    1.13 +  if Toplevel.is_toplevel state then Thy_Output.check_text txt state
    1.14    else raise Toplevel.UNDEF);
    1.15  
    1.16 -fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt);
    1.17 -val proof_markup = Toplevel.present_proof o check_text;
    1.18 +fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt);
    1.19 +val proof_markup = Toplevel.present_proof o Thy_Output.check_text;
    1.20  
    1.21  end;
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Aug 24 11:32:12 2012 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Aug 24 12:35:39 2012 +0200
     2.3 @@ -33,6 +33,7 @@
     2.4    val parse: Position.T -> string -> Toplevel.transition list
     2.5    type isar
     2.6    val isar: TextIO.instream -> bool -> isar
     2.7 +  val span_cmts: Token.T list -> Token.T list
     2.8    val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
     2.9    val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    2.10      (Toplevel.transition * Toplevel.transition list) list
    2.11 @@ -267,6 +268,22 @@
    2.12    |> toplevel_source term (SOME true) lookup_commands_dynamic;
    2.13  
    2.14  
    2.15 +(* side-comments *)
    2.16 +
    2.17 +local
    2.18 +
    2.19 +fun cmts (t1 :: t2 :: toks) =
    2.20 +      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    2.21 +      else cmts (t2 :: toks)
    2.22 +  | cmts toks = [];
    2.23 +
    2.24 +in
    2.25 +
    2.26 +val span_cmts = filter Token.is_proper #> cmts;
    2.27 +
    2.28 +end;
    2.29 +
    2.30 +
    2.31  (* read toplevel commands -- fail-safe *)
    2.32  
    2.33  fun read_span outer_syntax toks =
     3.1 --- a/src/Pure/PIDE/command.ML	Fri Aug 24 11:32:12 2012 +0200
     3.2 +++ b/src/Pure/PIDE/command.ML	Fri Aug 24 12:35:39 2012 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4    val memo_value: 'a -> 'a memo
     3.5    val memo_eval: 'a memo -> 'a
     3.6    val memo_result: 'a memo -> 'a
     3.7 -  val run_command: Toplevel.transition ->
     3.8 +  val run_command: Toplevel.transition * Token.T list ->
     3.9      Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
    3.10  end;
    3.11  
    3.12 @@ -73,6 +73,13 @@
    3.13    | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
    3.14    | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
    3.15  
    3.16 +fun check_cmts tr cmts st =
    3.17 +  Toplevel.setmp_thread_position tr
    3.18 +    (fn () => cmts
    3.19 +      |> maps (fn cmt =>
    3.20 +        (Thy_Output.check_text (Token.source_position_of cmt) st; [])
    3.21 +          handle exn => ML_Compiler.exn_messages exn)) ();
    3.22 +
    3.23  fun timing tr t =
    3.24    if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
    3.25  
    3.26 @@ -89,7 +96,7 @@
    3.27  
    3.28  in
    3.29  
    3.30 -fun run_command tr (st, malformed) =
    3.31 +fun run_command (tr, cmts) (st, malformed) =
    3.32    if malformed then ((Toplevel.toplevel, malformed), no_print)
    3.33    else
    3.34      let
    3.35 @@ -100,7 +107,9 @@
    3.36        val _ = Multithreading.interrupted ();
    3.37        val _ = Toplevel.status tr Isabelle_Markup.forked;
    3.38        val start = Timing.start ();
    3.39 -      val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    3.40 +      val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    3.41 +      val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
    3.42 +      val errs = errs1 @ errs2;
    3.43        val _ = timing tr (Timing.result start);
    3.44        val _ = Toplevel.status tr Isabelle_Markup.joined;
    3.45        val _ = List.app (Toplevel.error_msg tr) errs;
     4.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 24 11:32:12 2012 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 24 12:35:39 2012 +0200
     4.3 @@ -442,15 +442,19 @@
     4.4          else (I, init);
     4.5        val exec_id' = new_id ();
     4.6        val exec_id'_string = print_id exec_id';
     4.7 -      val tr =
     4.8 +      val cmd =
     4.9          Position.setmp_thread_data (Position.id_only exec_id'_string)
    4.10            (fn () =>
    4.11 -            #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    4.12 -            |> modify_init
    4.13 -            |> Toplevel.put_id exec_id'_string);
    4.14 +            let
    4.15 +              val tr =
    4.16 +                #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    4.17 +                |> modify_init
    4.18 +                |> Toplevel.put_id exec_id'_string;
    4.19 +              val cmts = Outer_Syntax.span_cmts span;
    4.20 +            in (tr, cmts) end);
    4.21        val exec' =
    4.22          Command.memo (fn () =>
    4.23 -          Command.run_command (tr ()) (fst (Command.memo_result (snd (snd command_exec)))));
    4.24 +          Command.run_command (cmd ()) (fst (Command.memo_result (snd (snd command_exec)))));
    4.25        val command_exec' = (command_id', (exec_id', exec'));
    4.26      in SOME (command_exec' :: execs, command_exec', init') end;
    4.27  
     5.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 24 11:32:12 2012 +0200
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 24 12:35:39 2012 +0200
     5.3 @@ -32,6 +32,7 @@
     5.4    val modes: string list Unsynchronized.ref
     5.5    val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
     5.6    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
     5.7 +  val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
     5.8    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     5.9      (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    5.10    val pretty_text: Proof.context -> string -> Pretty.T
    5.11 @@ -202,6 +203,11 @@
    5.12    end;
    5.13  
    5.14  
    5.15 +fun check_text (txt, pos) state =
    5.16 + (Position.report pos Isabelle_Markup.doc_source;
    5.17 +  ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
    5.18 +
    5.19 +
    5.20  
    5.21  (** present theory source **)
    5.22