# HG changeset patch
# User wenzelm
# Date 938958865 -7200
# Node ID 3edd32d588a6463f7ba8f3042e1aa42304b85bfa
# Parent  2e691e52281d77394e328635aa843b3b2206aa2c
improved theory_source presentation (hook);

diff -r 2e691e52281d -r 3edd32d588a6 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Oct 03 15:54:04 1999 +0200
+++ b/src/Pure/Thy/present.ML	Sun Oct 03 15:54:25 1999 +0200
@@ -3,9 +3,6 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Theory presentation abstract interface.
-
-TODO:
-  - presentation_modes: AND (!?);
 *)
 
 signature BASIC_PRESENT =
@@ -16,9 +13,31 @@
 signature PRESENT =
 sig
   include BROWSER_INFO
+  val theory_source_presenter:
+    (bool -> string -> (string, string list) Source.source * Position.T -> unit) -> unit
 end;
 
-structure Present: PRESENT = BrowserInfo;	(* FIXME *)
+structure Present: PRESENT =
+struct
+
+(*mostly fall back on BrowserInfo for the time being*)
+open BrowserInfo;
+
+
+(* theory source presenters *)
+
+local
+  val presenters =
+    ref ([]: (bool -> string -> (string, string list) Source.source  * Position.T -> unit) list);
+in
+  fun theory_source_presenter f = presenters := f :: ! presenters;
+  fun theory_source is_old name src = seq (fn f => f is_old name src) (! presenters);
+end;
+
+
+end;
+
+Present.theory_source_presenter BrowserInfo.theory_source;
 
 structure BasicPresent: BASIC_PRESENT = Present;
 open BasicPresent;