1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 03 16:19:57 2013 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 03 16:58:35 2013 +0200
     1.3 @@ -34,7 +34,9 @@
     1.4    val parse: Position.T -> string -> Toplevel.transition list
     1.5    type isar
     1.6    val isar: TextIO.instream -> bool -> isar
     1.7 -  val read_span: outer_syntax -> Token.T list -> Toplevel.transition
     1.8 +  val side_comments: Token.T list -> Token.T list
     1.9 +  val command_reports: outer_syntax -> Token.T -> (Position.report * string) list
    1.10 +  val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list
    1.11  end;
    1.12  
    1.13  structure Outer_Syntax: OUTER_SYNTAX =
    1.14 @@ -276,41 +278,31 @@
    1.15    |> toplevel_source term (SOME true) lookup_commands_dynamic;
    1.16  
    1.17  
    1.18 -(* read command span -- fail-safe *)
    1.19 +(* side-comments *)
    1.20  
    1.21 -fun read_span outer_syntax toks =
    1.22 -  let
    1.23 -    val commands = lookup_commands outer_syntax;
    1.24 +fun cmts (t1 :: t2 :: toks) =
    1.25 +      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    1.26 +      else cmts (t2 :: toks)
    1.27 +  | cmts _ = [];
    1.28  
    1.29 -    val proper_range = Position.set_range (Command.proper_range toks);
    1.30 -    val pos =
    1.31 -      (case find_first Token.is_command toks of
    1.32 -        SOME tok => Token.position_of tok
    1.33 -      | NONE => proper_range);
    1.34 +val side_comments = filter Token.is_proper #> cmts;
    1.35  
    1.36 -    fun command_reports tok =
    1.37 -      if Token.is_command tok then
    1.38 -        let val name = Token.content_of tok in
    1.39 -          (case commands name of
    1.40 -            NONE => []
    1.41 -          | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
    1.42 -        end
    1.43 -      else [];
    1.44  
    1.45 -    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
    1.46 -    val _ = Position.reports_text (token_reports @ maps command_reports toks);
    1.47 -  in
    1.48 -    if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    1.49 -    else
    1.50 -      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
    1.51 -        [tr] =>
    1.52 -          if Keyword.is_control (Toplevel.name_of tr) then
    1.53 -            Toplevel.malformed pos "Illegal control command"
    1.54 -          else tr
    1.55 -      | [] => Toplevel.ignored (Position.set_range (Command.range toks))
    1.56 -      | _ => Toplevel.malformed proper_range "Exactly one command expected")
    1.57 -      handle ERROR msg => Toplevel.malformed proper_range msg
    1.58 -  end;
    1.59 +(* read commands *)
    1.60 +
    1.61 +fun command_reports outer_syntax tok =
    1.62 +  if Token.is_command tok then
    1.63 +    let val name = Token.content_of tok in
    1.64 +      (case lookup_commands outer_syntax name of
    1.65 +        NONE => []
    1.66 +      | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
    1.67 +    end
    1.68 +  else [];
    1.69 +
    1.70 +fun read_spans outer_syntax toks =
    1.71 +  Source.of_list toks
    1.72 +  |> toplevel_source false NONE (K (lookup_commands outer_syntax))
    1.73 +  |> Source.exhaust;
    1.74  
    1.75  end;
    1.76  

     2.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 03 16:19:57 2013 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 03 16:58:35 2013 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4    val memo_value: 'a -> 'a memo
     2.5    val memo_eval: 'a memo -> 'a
     2.6    val memo_result: 'a memo -> 'a
     2.7 +  val read: span -> Toplevel.transition
     2.8    val eval: span -> Toplevel.transition ->
     2.9      Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
    2.10    val no_print: unit lazy
    2.11 @@ -62,27 +63,33 @@
    2.12  end;
    2.13  
    2.14  
    2.15 -(* side-comments *)
    2.16 +(* read *)
    2.17  
    2.18 -local
    2.19 +fun read span =
    2.20 +  let
    2.21 +    val outer_syntax = #2 (Outer_Syntax.get_syntax ());
    2.22 +    val command_reports = Outer_Syntax.command_reports outer_syntax;
    2.23  
    2.24 -fun cmts (t1 :: t2 :: toks) =
    2.25 -      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    2.26 -      else cmts (t2 :: toks)
    2.27 -  | cmts _ = [];
    2.28 +    val proper_range = Position.set_range (proper_range span);
    2.29 +    val pos =
    2.30 +      (case find_first Token.is_command span of
    2.31 +        SOME tok => Token.position_of tok
    2.32 +      | NONE => proper_range);
    2.33  
    2.34 -val span_cmts = filter Token.is_proper #> cmts;
    2.35 -
    2.36 -in
    2.37 -
    2.38 -fun check_cmts span tr st' =
    2.39 -  Toplevel.setmp_thread_position tr
    2.40 -    (fn () =>
    2.41 -      span_cmts span |> maps (fn cmt =>
    2.42 -        (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
    2.43 -          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    2.44 -
    2.45 -end;
    2.46 +    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
    2.47 +    val _ = Position.reports_text (token_reports @ maps command_reports span);
    2.48 +  in
    2.49 +    if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    2.50 +    else
    2.51 +      (case Outer_Syntax.read_spans outer_syntax span of
    2.52 +        [tr] =>
    2.53 +          if Keyword.is_control (Toplevel.name_of tr) then
    2.54 +            Toplevel.malformed pos "Illegal control command"
    2.55 +          else tr
    2.56 +      | [] => Toplevel.ignored (Position.set_range (range span))
    2.57 +      | _ => Toplevel.malformed proper_range "Exactly one command expected")
    2.58 +      handle ERROR msg => Toplevel.malformed proper_range msg
    2.59 +  end;
    2.60  
    2.61  
    2.62  (* eval *)
    2.63 @@ -95,6 +102,13 @@
    2.64        (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    2.65    else Toplevel.command_errors int tr st;
    2.66  
    2.67 +fun check_cmts span tr st' =
    2.68 +  Toplevel.setmp_thread_position tr
    2.69 +    (fn () =>
    2.70 +      Outer_Syntax.side_comments span |> maps (fn cmt =>
    2.71 +        (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
    2.72 +          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    2.73 +
    2.74  fun proof_status tr st =
    2.75    (case try Toplevel.proof_of st of
    2.76      SOME prf => Toplevel.status tr (Proof.status_markup prf)

     3.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 03 16:19:57 2013 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 03 16:58:35 2013 +0200
     3.3 @@ -450,7 +450,7 @@
     3.4        val read =
     3.5          Position.setmp_thread_data (Position.id_only exec_id'_string)
     3.6            (fn () =>
     3.7 -            Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
     3.8 +            Command.read span
     3.9              |> modify_init
    3.10              |> Toplevel.put_id exec_id'_string);
    3.11        val exec' =

     4.1 --- a/src/Pure/ROOT.ML	Wed Jul 03 16:19:57 2013 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Wed Jul 03 16:58:35 2013 +0200
     4.3 @@ -262,10 +262,10 @@
     4.4  use "System/isabelle_system.ML";
     4.5  use "Thy/term_style.ML";
     4.6  use "Thy/thy_output.ML";
     4.7 -use "PIDE/command.ML";
     4.8  use "Isar/outer_syntax.ML";
     4.9  use "General/graph_display.ML";
    4.10  use "Thy/present.ML";
    4.11 +use "PIDE/command.ML";
    4.12  use "Thy/thy_load.ML";
    4.13  use "Thy/thy_info.ML";
    4.14  use "PIDE/document.ML";

     5.1 --- a/src/Pure/Thy/thy_load.ML	Wed Jul 03 16:19:57 2013 +0200
     5.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Jul 03 16:58:35 2013 +0200
     5.3 @@ -217,7 +217,7 @@
     5.4    let
     5.5      fun prepare_span span =
     5.6        Thy_Syntax.span_content span
     5.7 -      |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
     5.8 +      |> Command.read
     5.9        |> Toplevel.modify_init init
    5.10        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    5.11