src/Pure/Isar/outer_syntax.ML
changeset 15144 85929e1b307d
parent 14981 e73f8140af78
child 15156 daa9f645a26e
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 18 16:03:15 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 18 16:04:39 2004 +0200
     1.3 @@ -61,8 +61,9 @@
     1.4    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
     1.5    val load_thy: string -> bool -> bool -> Path.T -> unit
     1.6    val isar: bool -> bool -> unit Toplevel.isar
     1.7 -  val isar_readstring: Position.T -> string -> (string list) Toplevel.isar
     1.8 -  val read: string -> (string * OuterLex.token list * Toplevel.transition) list
     1.9 +  val scan: string -> OuterLex.token list
    1.10 +  val read: OuterLex.token list -> 
    1.11 +		(string * OuterLex.token list * Toplevel.transition) list
    1.12  end;
    1.13  
    1.14  structure OuterSyntax: OUTER_SYNTAX =
    1.15 @@ -264,27 +265,21 @@
    1.16    |> toplevel_source term false true get_parser;
    1.17  
    1.18  
    1.19 -(* string source of transformers with trace (for Proof General) *)
    1.20 -
    1.21 -fun isar_readstring pos str =
    1.22 -  Source.of_string str
    1.23 -  |> Symbol.source false
    1.24 -  |> T.source false get_lexicons pos
    1.25 -  |> toplevel_source false true true get_parser;
    1.26 +(* scan text,  read tokens with trace (for Proof General) *)
    1.27  
    1.28 -
    1.29 -(* read text -- with trace of source *)
    1.30 +fun scan str =
    1.31 + Source.of_string str
    1.32 + |> Symbol.source false
    1.33 + |> T.source false get_lexicons Position.none
    1.34 + |> Source.exhaust
    1.35  
    1.36 -fun read str =
    1.37 -  Source.of_string str
    1.38 -  |> Symbol.source false
    1.39 -  |> T.source false get_lexicons Position.none
    1.40 +fun read toks =
    1.41 +  Source.of_list toks
    1.42    |> toplevel_source false true true get_parser
    1.43    |> Source.exhaust
    1.44    |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
    1.45  
    1.46  
    1.47 -
    1.48  (** read theory **)
    1.49  
    1.50  (* check_text *)