improved theory_source presentation;
authorwenzelm
Sun, 03 Oct 1999 15:54:04 +0200
changeset 7684 2e691e52281d
parent 7683 e74f43f1d8a3
child 7685 3edd32d588a6
improved theory_source presentation;
src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Sun Oct 03 15:52:53 1999 +0200
+++ b/src/Pure/Thy/browser_info.ML	Sun Oct 03 15:54:04 1999 +0200
@@ -15,7 +15,7 @@
   include BASIC_BROWSER_INFO
   val init: bool -> string list -> string -> Url.T option * bool -> unit
   val finish: unit -> unit
-  val theory_source: string -> (string, 'a) Source.source -> unit
+  val theory_source: bool -> string -> (string, string list) Source.source * Position.T -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
   val end_theory: string -> unit
   val result: string -> string -> thm -> unit
@@ -304,7 +304,7 @@
 
 (* theory elements *)
 
-fun theory_source name src = with_session () (fn _ =>
+fun theory_source is_old name (src, _) = with_session () (fn _ =>
   (init_theory_info name empty_theory_info; add_source name (HTML.source src)));