1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 03 16:19:57 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 03 16:58:35 2013 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val memo_value: 'a -> 'a memo
     1.5    val memo_eval: 'a memo -> 'a
     1.6    val memo_result: 'a memo -> 'a
     1.7 +  val read: span -> Toplevel.transition
     1.8    val eval: span -> Toplevel.transition ->
     1.9      Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
    1.10    val no_print: unit lazy
    1.11 @@ -62,27 +63,33 @@
    1.12  end;
    1.13  
    1.14  
    1.15 -(* side-comments *)
    1.16 +(* read *)
    1.17  
    1.18 -local
    1.19 +fun read span =
    1.20 +  let
    1.21 +    val outer_syntax = #2 (Outer_Syntax.get_syntax ());
    1.22 +    val command_reports = Outer_Syntax.command_reports outer_syntax;
    1.23  
    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 +    val proper_range = Position.set_range (proper_range span);
    1.29 +    val pos =
    1.30 +      (case find_first Token.is_command span of
    1.31 +        SOME tok => Token.position_of tok
    1.32 +      | NONE => proper_range);
    1.33  
    1.34 -val span_cmts = filter Token.is_proper #> cmts;
    1.35 -
    1.36 -in
    1.37 -
    1.38 -fun check_cmts span tr st' =
    1.39 -  Toplevel.setmp_thread_position tr
    1.40 -    (fn () =>
    1.41 -      span_cmts span |> maps (fn cmt =>
    1.42 -        (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
    1.43 -          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    1.44 -
    1.45 -end;
    1.46 +    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
    1.47 +    val _ = Position.reports_text (token_reports @ maps command_reports span);
    1.48 +  in
    1.49 +    if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    1.50 +    else
    1.51 +      (case Outer_Syntax.read_spans outer_syntax span of
    1.52 +        [tr] =>
    1.53 +          if Keyword.is_control (Toplevel.name_of tr) then
    1.54 +            Toplevel.malformed pos "Illegal control command"
    1.55 +          else tr
    1.56 +      | [] => Toplevel.ignored (Position.set_range (range span))
    1.57 +      | _ => Toplevel.malformed proper_range "Exactly one command expected")
    1.58 +      handle ERROR msg => Toplevel.malformed proper_range msg
    1.59 +  end;
    1.60  
    1.61  
    1.62  (* eval *)
    1.63 @@ -95,6 +102,13 @@
    1.64        (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    1.65    else Toplevel.command_errors int tr st;
    1.66  
    1.67 +fun check_cmts span tr st' =
    1.68 +  Toplevel.setmp_thread_position tr
    1.69 +    (fn () =>
    1.70 +      Outer_Syntax.side_comments span |> maps (fn cmt =>
    1.71 +        (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
    1.72 +          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    1.73 +
    1.74  fun proof_status tr st =
    1.75    (case try Toplevel.proof_of st of
    1.76      SOME prf => Toplevel.status tr (Proof.status_markup prf)