present token source;
authorwenzelm
Tue Oct 05 15:37:44 1999 +0200 (1999-10-05)
changeset 77353e5ff3806831
parent 7734 9c098c777926
child 7736 847cd420a928
present token source;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Oct 05 15:36:56 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Oct 05 15:37:44 1999 +0200
     1.3 @@ -50,8 +50,6 @@
     1.4    val print_help: Toplevel.transition -> Toplevel.transition
     1.5    val add_keywords: string list -> unit
     1.6    val add_parsers: parser list -> unit
     1.7 -  val token_source: (string, 'a) Source.source * Position.T -> (OuterLex.token,
     1.8 -    Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) Source.source
     1.9    val theory_header: token list -> (string * string list * (string * bool) list) * token list
    1.10    val deps_thy: string -> Path.T -> string list * Path.T list
    1.11    val load_thy: string -> bool -> bool -> Path.T -> unit
    1.12 @@ -289,11 +287,12 @@
    1.13  
    1.14  fun deps_thy name path =
    1.15    let
    1.16 -    val src = File.source path;
    1.17 +    val src = Source.of_string (File.read path);
    1.18 +    val pos = Path.position path;
    1.19      val (name', parents, files) =
    1.20        (*Note: old style headers dynamically depend on the current lexicon :-( *)
    1.21 -      if is_old_theory src then scan_header ThySyn.get_lexicon (Scan.error old_header) src
    1.22 -      else scan_header (K header_lexicon) (Scan.error new_header) src;
    1.23 +      if is_old_theory (src, pos) then scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
    1.24 +      else scan_header (K header_lexicon) (Scan.error new_header) (src, pos);
    1.25  
    1.26      val ml_path = ThyLoad.ml_path name;
    1.27      val ml_file = if is_none (ThyLoad.check_file ml_path) then [] else [ml_path];
    1.28 @@ -336,12 +335,19 @@
    1.29  
    1.30  fun run_thy name path =
    1.31    let
    1.32 -    val (src, pos) = File.source path;
    1.33 -    val is_old = is_old_theory (src, pos);
    1.34 +    val text = explode (File.read path);
    1.35 +    val src = Source.of_list text;
    1.36 +    val pos = Path.position path;
    1.37 +
    1.38 +    fun present_toks () =
    1.39 +      Source.exhaust (token_source (Source.of_list (Library.untabify text), pos));
    1.40 +    fun present_text () =
    1.41 +      Source.exhaust (Symbol.source false (Source.of_list (Library.untabify text)));
    1.42    in
    1.43 -    Present.theory_source is_old name (src, pos);
    1.44 -    if is_old then ThySyn.load_thy name (Source.exhaust src)
    1.45 -    else Toplevel.excursion_error (parse_thy (src, pos))
    1.46 +    Present.init_theory name;
    1.47 +    if is_old_theory (src, pos) then ThySyn.load_thy name text
    1.48 +    else (Toplevel.excursion_error (parse_thy (src, pos)); Present.token_source name present_toks);
    1.49 +    Present.verbatim_source name present_text
    1.50    end;
    1.51  
    1.52  fun load_thy name ml time path =