# HG changeset patch
# User aspinall
# Date 1092837879 -7200
# Node ID 85929e1b307d59b4485a64ef14137b6f298b0cf7
# Parent  05b5995f214e6b813fd72e0ba0aba4f6c2f0dfac
Remove isar_readstring.  Split read into scanner and parser.

diff -r 05b5995f214e -r 85929e1b307d src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 18 16:03:15 2004 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 18 16:04:39 2004 +0200
@@ -61,8 +61,9 @@
   val deps_thy: string -> bool -> Path.T -> string list * Path.T list
   val load_thy: string -> bool -> bool -> Path.T -> unit
   val isar: bool -> bool -> unit Toplevel.isar
-  val isar_readstring: Position.T -> string -> (string list) Toplevel.isar
-  val read: string -> (string * OuterLex.token list * Toplevel.transition) list
+  val scan: string -> OuterLex.token list
+  val read: OuterLex.token list -> 
+		(string * OuterLex.token list * Toplevel.transition) list
 end;
 
 structure OuterSyntax: OUTER_SYNTAX =
@@ -264,27 +265,21 @@
   |> toplevel_source term false true get_parser;
 
 
-(* string source of transformers with trace (for Proof General) *)
-
-fun isar_readstring pos str =
-  Source.of_string str
-  |> Symbol.source false
-  |> T.source false get_lexicons pos
-  |> toplevel_source false true true get_parser;
+(* scan text,  read tokens with trace (for Proof General) *)
 
-
-(* read text -- with trace of source *)
+fun scan str =
+ Source.of_string str
+ |> Symbol.source false
+ |> T.source false get_lexicons Position.none
+ |> Source.exhaust
 
-fun read str =
-  Source.of_string str
-  |> Symbol.source false
-  |> T.source false get_lexicons Position.none
+fun read toks =
+  Source.of_list toks
   |> toplevel_source false true true get_parser
   |> Source.exhaust
   |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
 
 
-
 (** read theory **)
 
 (* check_text *)