# HG changeset patch
# User wenzelm
# Date 1279831171 -7200
# Node ID 4857eab312982de5904646ae99bf806ccfd776cb
# Parent  965537d86fccdd4f31abd8e2d7fdeb9eef988e5b
generic external source files -- nothing special about ML here;

diff -r 965537d86fcc -r 4857eab31298 lib/html/isabelle.css
--- a/lib/html/isabelle.css	Thu Jul 22 22:31:20 2010 +0200
+++ b/lib/html/isabelle.css	Thu Jul 22 22:39:31 2010 +0200
@@ -5,8 +5,8 @@
 .head     { background-color: #FFFFFF; }
 .source   { background-color: #F0F0F0; padding: 10px; }
 
-.mlsource { background-color: #F0F0F0; padding: 10px; }
-.mlfooter { background-color: #FFFFFF; }
+.external_source { background-color: #F0F0F0; padding: 10px; }
+.external_footer { background-color: #FFFFFF; }
 
 .theories { background-color: #F0F0F0; padding: 10px; }
 .sessions { background-color: #F0F0F0; padding: 10px; }
diff -r 965537d86fcc -r 4857eab31298 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Jul 22 22:31:20 2010 +0200
+++ b/src/Pure/Thy/html.ML	Thu Jul 22 22:39:31 2010 +0200
@@ -30,7 +30,7 @@
   val theory_source: text -> text
   val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
     (Url.T * Url.T * bool) list -> text -> text
-  val ml_file: Url.T -> string -> text
+  val external_file: Url.T -> string -> text
 end;
 
 structure HTML: HTML =
@@ -379,13 +379,13 @@
 end;
 
 
-(* ML file *)
+(* external file *)
 
-fun ml_file path str =
+fun external_file path str =
   begin_document ("File " ^ Url.implode path) ^
-  "\n</div>\n<hr/><div class=\"mlsource\">\n" ^
+  "\n</div>\n<hr/><div class=\"external_source\">\n" ^
   verbatim str ^
-  "\n</div>\n<hr/>\n<div class=\"mlfooter\">" ^
+  "\n</div>\n<hr/>\n<div class=\"external_footer\">" ^
   end_document;
 
 end;
diff -r 965537d86fcc -r 4857eab31298 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Jul 22 22:31:20 2010 +0200
+++ b/src/Pure/Thy/present.ML	Thu Jul 22 22:39:31 2010 +0200
@@ -466,7 +466,7 @@
         val base = Path.base path;
         val base_html = html_ext base;
         val _ = add_file (Path.append html_prefix base_html,
-          HTML.ml_file (Url.File base) (File.read path));
+          HTML.external_file (Url.File base) (File.read path));
       in (Url.File base_html, Url.File raw_path, loadit) end);
 
     fun prep_html_source (tex_source, html_source, html) =