1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Oct 19 21:52:44 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Oct 19 21:52:45 2005 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4    let
     1.5      val src = Source.of_string (File.read path);
     1.6      val pos = Path.position path;
     1.7 -    val (name', parents, files) = ThyHeader.scan (src, pos);
     1.8 +    val (name', parents, files) = ThyHeader.read (src, pos);
     1.9      val ml_path = ThyLoad.ml_path name;
    1.10      val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    1.11    in
    1.12 @@ -270,32 +270,20 @@
    1.13  
    1.14  fun run_thy name path =
    1.15    let
    1.16 -    val pos = Path.position path;
    1.17 -    val text = Library.untabify (explode (File.read path));
    1.18 -    val text_src = Source.of_list text;
    1.19 -    fun present_text () = Source.exhaust (Symbol.source false text_src);
    1.20 +    val text = Source.of_list (Library.untabify (explode (File.read path)));
    1.21 +    val _ = Present.init_theory name;
    1.22 +    val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text));
    1.23 +    val toks = text
    1.24 +      |> Symbol.source false
    1.25 +      |> T.source false (K (get_lexicons ())) (Path.position path)
    1.26 +      |> Source.exhausted;
    1.27 +    val trs = toks
    1.28 +      |> toplevel_source false false false (K (get_parser ()))
    1.29 +      |> Source.exhaust;
    1.30    in
    1.31 -    Present.init_theory name;
    1.32 -    Present.verbatim_source name present_text;
    1.33 -    if ThyHeader.is_old (text_src, pos) then
    1.34 -     (warning ("Non-Isar file format for theory " ^ quote name ^ " -- deprecated");
    1.35 -      ThySyn.load_thy name text;
    1.36 -      Present.old_symbol_source name present_text)   (*note: text presented twice*)
    1.37 -    else
    1.38 -      let
    1.39 -        val tok_src = text_src
    1.40 -          |> Symbol.source false
    1.41 -          |> T.source false (K (get_lexicons ())) pos
    1.42 -          |> Source.exhausted;
    1.43 -        val trs =
    1.44 -          tok_src
    1.45 -          |> toplevel_source false false false (K (get_parser ()))
    1.46 -          |> Source.exhaust;
    1.47 -      in
    1.48 -        IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs tok_src
    1.49 -        |> Buffer.content
    1.50 -        |> Present.theory_output name
    1.51 -      end
    1.52 +    IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
    1.53 +    |> Buffer.content
    1.54 +    |> Present.theory_output name
    1.55    end;
    1.56  
    1.57  in