# HG changeset patch
# User wenzelm
# Date 1218653850 -7200
# Node ID b1bf607e06c295ca4fb15ff181d1b4220edeadba
# Parent  be5372792b084a390dd42529b7d418b7e39afe70
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;

diff -r be5372792b08 -r b1bf607e06c2 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 13 20:57:28 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 13 20:57:30 2008 +0200
@@ -225,7 +225,6 @@
   |> toplevel_source term (SOME true) get_parser;
 
 
-
 (* prepare toplevel commands -- fail-safe *)
 
 val not_singleton = "Exactly one command expected";
@@ -256,16 +255,17 @@
 fun load_thy name pos text time =
   let
     val (lexs, parser) = get_syntax ();
-    val text_src = Source.of_list (Library.untabify text);
 
     val _ = Present.init_theory name;
-    val _ = Present.verbatim_source name
-      (fn () => Source.exhaust (Symbol.source {do_recover = false} text_src));
-    val toks = Source.exhausted (ThyEdit.token_source lexs pos text_src);
+
+    val toks = Source.exhausted (ThyEdit.token_source lexs pos (Source.of_list text));
     val spans = Source.exhaust (ThyEdit.span_source toks);
     val _ = List.app ThyEdit.report_span spans;
     val trs = map (prepare_span parser) spans |> filter #2 |> map #1;
 
+    val _ = Present.theory_source name
+      (fn () => HTML.html_mode (implode o map ThyEdit.present_span) spans);
+
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
     val _ = cond_timeit time "" (fn () =>
       ThyOutput.process_thy (#1 lexs) OuterKeyword.command_tags is_markup trs toks