# HG changeset patch
# User wenzelm
# Date 1217974346 -7200
# Node ID 24d0e890b43238e057b9f4cb8dca1f44e44fb679
# Parent  f7cdde18aeb3d67db4e5be27a76f32af97e470d3
T.end_position_of;
tuned;

diff -r f7cdde18aeb3 -r 24d0e890b432 src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Wed Aug 06 00:12:21 2008 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Wed Aug 06 00:12:26 2008 +0200
@@ -76,7 +76,7 @@
   | span_range (_, toks) =
       let
         val start_pos = T.position_of (hd toks);
-        val end_pos = #2 (T.range_of (List.last toks));
+        val end_pos = T.end_position_of (List.last toks);
       in (start_pos, end_pos) end;
 
 
@@ -124,7 +124,7 @@
 (* HTML presentation -- example *)
 
 fun present_html inpath outpath =
-  Source.exhaust (span_source (Path.position inpath) (Source.of_string (File.read inpath)))
+  parse_spans (Path.position inpath) (Source.of_string (File.read inpath))
   |> HTML.html_mode (implode o map present_span)
   |> enclose
     (HTML.begin_document (Path.implode (Path.base inpath)) ^ "<div class=\"source\"><pre>")