src/Pure/Isar/outer_syntax.ML
changeset 16195 0eb3c15298cd
parent 15989 80dd2f5780df
child 16727 e264077b68a7
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Jun 02 18:29:54 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Jun 02 18:29:55 2005 +0200
     1.3 @@ -64,9 +64,8 @@
     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 scan: string -> OuterLex.token list  
     1.8 -  val read: OuterLex.token list -> 
     1.9 -		(string * OuterLex.token list * Toplevel.transition) list
    1.10 +  val scan: string -> OuterLex.token list
    1.11 +  val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list
    1.12  end;
    1.13  
    1.14  structure OuterSyntax : OUTER_SYNTAX  =
    1.15 @@ -268,13 +267,16 @@
    1.16    |> toplevel_source term false true get_parser;
    1.17  
    1.18  
    1.19 -(* scan text,  read tokens with trace (for Proof General) *)
    1.20 +(* scan text *)
    1.21  
    1.22  fun scan str =
    1.23 - Source.of_string str
    1.24 - |> Symbol.source false
    1.25 - |> T.source true get_lexicons Position.none
    1.26 - |> Source.exhaust
    1.27 +  Source.of_string str
    1.28 +  |> Symbol.source false
    1.29 +  |> T.source true get_lexicons Position.none
    1.30 +  |> Source.exhaust;
    1.31 +
    1.32 +
    1.33 +(* read tokens with trace *)
    1.34  
    1.35  fun read toks =
    1.36    Source.of_list toks
    1.37 @@ -283,6 +285,7 @@
    1.38    |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
    1.39  
    1.40  
    1.41 +
    1.42  (** read theory **)
    1.43  
    1.44  (* check_text *)