# HG changeset patch
# User wenzelm
# Date 938958844 -7200
# Node ID 2e691e52281d77394e328635aa843b3b2206aa2c
# Parent  e74f43f1d8a3056610a68343fefe706004392b75
improved theory_source presentation;

diff -r e74f43f1d8a3 -r 2e691e52281d 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)));