# HG changeset patch
# User wenzelm
# Date 1218653860 -7200
# Node ID a084895d8b91f8590fad9e7f41c6304ec1341693
# Parent  8f727f7c8c1d3e3e0db02fbf80043b9021a92113
removed obsolete present_html -- now part of regular theory presentation;

diff -r 8f727f7c8c1d -r a084895d8b91 src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Wed Aug 13 20:57:39 2008 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Wed Aug 13 20:57:40 2008 +0200
@@ -23,7 +23,6 @@
   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
   val present_span: span -> output
   val report_span: span -> unit
-  val present_html: Path.T -> Path.T -> unit
 end;
 
 structure ThyEdit: THY_EDIT =
@@ -149,15 +148,4 @@
 
 end;
 
-
-(* HTML presentation -- example *)
-
-fun present_html inpath outpath =
-  parse_spans (OuterKeyword.get_lexicons ()) (Path.position inpath) (File.read inpath)
-  |> HTML.html_mode (implode o map present_span)
-  |> enclose
-    (HTML.begin_document (Path.implode (Path.base inpath)) ^ "<div class=\"source\"><pre>")
-    ("</pre></div>" ^ HTML.end_document)
-  |> File.write outpath;
-
 end;