# HG changeset patch
# User wenzelm
# Date 1197062393 -3600
# Node ID 6623674df89716e6c79c0e7f2b6db1378a369eba
# Parent  22869d9d545b9c305e55a34dffa9cda16ec5c44e
added off-line parse;
read: no recovery on non-interactive source, yields proper errors;

diff -r 22869d9d545b -r 6623674df897 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Dec 07 22:19:51 2007 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Dec 07 22:19:53 2007 +0100
@@ -43,6 +43,7 @@
   val check_text: string * Position.T -> Toplevel.node option -> unit
   val scan: string -> OuterLex.token list
   val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list
+  val parse: Position.T -> string -> Toplevel.transition list
   val isar: bool -> unit Toplevel.isar
 end;
 
@@ -231,23 +232,30 @@
   end;
 
 
-(* scan text *)
+(* off-line scanning/parsing *)
 
+(*tokens*)
 fun scan str =
   Source.of_string str
   |> Symbol.source false
   |> T.source (SOME false) get_lexicons Position.none
   |> Source.exhaust;
 
-
-(* read tokens with trace *)
-
+(*commands from tokens, with trace*)
 fun read toks =
   Source.of_list toks
-  |> toplevel_source false true (SOME false) get_parser
+  |> toplevel_source false true NONE get_parser
   |> Source.exhaust
   |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
 
+(*commands from string, without trace*)
+fun parse pos str =
+  Source.of_string str
+  |> Symbol.source false
+  |> T.source (SOME false) get_lexicons pos
+  |> toplevel_source false false NONE get_parser
+  |> Source.exhaust;
+
 
 (* interactive source of toplevel transformers *)