--- a/src/Pure/Isar/outer_syntax.ML Tue Apr 14 22:54:07 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Apr 15 11:47:29 2015 +0200
@@ -177,22 +177,18 @@
| SOME (Command {command_parser = Limited_Parser parse, ...}) =>
before_command :|-- (fn limited =>
Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
- | NONE =>
- Scan.succeed
- (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
+ | NONE => Scan.fail_with (fn _ => fn _ => err_command "Undefined command " name [pos]))
end);
val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
-in
-
fun commands_source thy =
Token.source_proper #>
Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) #>
Source.map_filter I #>
Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs));
-end;
+in
fun parse thy pos str =
Source.of_string str
@@ -206,6 +202,8 @@
|> commands_source thy
|> Source.exhaust;
+end;
+
(* parse spans *)