--- a/src/Pure/Isar/outer_syntax.ML Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 03 16:58:35 2013 +0200
@@ -34,7 +34,9 @@
val parse: Position.T -> string -> Toplevel.transition list
type isar
val isar: TextIO.instream -> bool -> isar
- val read_span: outer_syntax -> Token.T list -> Toplevel.transition
+ val side_comments: Token.T list -> Token.T list
+ val command_reports: outer_syntax -> Token.T -> (Position.report * string) list
+ val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -276,41 +278,31 @@
|> toplevel_source term (SOME true) lookup_commands_dynamic;
-(* read command span -- fail-safe *)
-
-fun read_span outer_syntax toks =
- let
- val commands = lookup_commands outer_syntax;
+(* side-comments *)
- val proper_range = Position.set_range (Command.proper_range toks);
- val pos =
- (case find_first Token.is_command toks of
- SOME tok => Token.position_of tok
- | NONE => proper_range);
+fun cmts (t1 :: t2 :: toks) =
+ if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
+ else cmts (t2 :: toks)
+ | cmts _ = [];
+
+val side_comments = filter Token.is_proper #> cmts;
+
+
+(* read commands *)
- fun command_reports tok =
- if Token.is_command tok then
- let val name = Token.content_of tok in
- (case commands name of
- NONE => []
- | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
- end
- else [];
+fun command_reports outer_syntax tok =
+ if Token.is_command tok then
+ let val name = Token.content_of tok in
+ (case lookup_commands outer_syntax name of
+ NONE => []
+ | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
+ end
+ else [];
- val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
- val _ = Position.reports_text (token_reports @ maps command_reports toks);
- in
- if is_malformed then Toplevel.malformed pos "Malformed command syntax"
- else
- (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
- [tr] =>
- if Keyword.is_control (Toplevel.name_of tr) then
- Toplevel.malformed pos "Illegal control command"
- else tr
- | [] => Toplevel.ignored (Position.set_range (Command.range toks))
- | _ => Toplevel.malformed proper_range "Exactly one command expected")
- handle ERROR msg => Toplevel.malformed proper_range msg
- end;
+fun read_spans outer_syntax toks =
+ Source.of_list toks
+ |> toplevel_source false NONE (K (lookup_commands outer_syntax))
+ |> Source.exhaust;
end;
--- a/src/Pure/PIDE/command.ML Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/PIDE/command.ML Wed Jul 03 16:58:35 2013 +0200
@@ -14,6 +14,7 @@
val memo_value: 'a -> 'a memo
val memo_eval: 'a memo -> 'a
val memo_result: 'a memo -> 'a
+ val read: span -> Toplevel.transition
val eval: span -> Toplevel.transition ->
Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
val no_print: unit lazy
@@ -62,27 +63,33 @@
end;
-(* side-comments *)
-
-local
+(* read *)
-fun cmts (t1 :: t2 :: toks) =
- if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
- else cmts (t2 :: toks)
- | cmts _ = [];
+fun read span =
+ let
+ val outer_syntax = #2 (Outer_Syntax.get_syntax ());
+ val command_reports = Outer_Syntax.command_reports outer_syntax;
-val span_cmts = filter Token.is_proper #> cmts;
+ val proper_range = Position.set_range (proper_range span);
+ val pos =
+ (case find_first Token.is_command span of
+ SOME tok => Token.position_of tok
+ | NONE => proper_range);
-in
-
-fun check_cmts span tr st' =
- Toplevel.setmp_thread_position tr
- (fn () =>
- span_cmts span |> maps (fn cmt =>
- (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
- handle exn => ML_Compiler.exn_messages_ids exn)) ();
-
-end;
+ val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
+ val _ = Position.reports_text (token_reports @ maps command_reports span);
+ in
+ if is_malformed then Toplevel.malformed pos "Malformed command syntax"
+ else
+ (case Outer_Syntax.read_spans outer_syntax span of
+ [tr] =>
+ if Keyword.is_control (Toplevel.name_of tr) then
+ Toplevel.malformed pos "Illegal control command"
+ else tr
+ | [] => Toplevel.ignored (Position.set_range (range span))
+ | _ => Toplevel.malformed proper_range "Exactly one command expected")
+ handle ERROR msg => Toplevel.malformed proper_range msg
+ end;
(* eval *)
@@ -95,6 +102,13 @@
(fn () => Toplevel.command_exception int tr st); ([], SOME st))
else Toplevel.command_errors int tr st;
+fun check_cmts span tr st' =
+ Toplevel.setmp_thread_position tr
+ (fn () =>
+ Outer_Syntax.side_comments span |> maps (fn cmt =>
+ (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
+ handle exn => ML_Compiler.exn_messages_ids exn)) ();
+
fun proof_status tr st =
(case try Toplevel.proof_of st of
SOME prf => Toplevel.status tr (Proof.status_markup prf)
--- a/src/Pure/PIDE/document.ML Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/PIDE/document.ML Wed Jul 03 16:58:35 2013 +0200
@@ -450,7 +450,7 @@
val read =
Position.setmp_thread_data (Position.id_only exec_id'_string)
(fn () =>
- Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
+ Command.read span
|> modify_init
|> Toplevel.put_id exec_id'_string);
val exec' =
--- a/src/Pure/ROOT.ML Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/ROOT.ML Wed Jul 03 16:58:35 2013 +0200
@@ -262,10 +262,10 @@
use "System/isabelle_system.ML";
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
-use "PIDE/command.ML";
use "Isar/outer_syntax.ML";
use "General/graph_display.ML";
use "Thy/present.ML";
+use "PIDE/command.ML";
use "Thy/thy_load.ML";
use "Thy/thy_info.ML";
use "PIDE/document.ML";
--- a/src/Pure/Thy/thy_load.ML Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML Wed Jul 03 16:58:35 2013 +0200
@@ -217,7 +217,7 @@
let
fun prepare_span span =
Thy_Syntax.span_content span
- |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
+ |> Command.read
|> Toplevel.modify_init init
|> (fn tr => Toplevel.put_timing (last_timing tr) tr);