--- a/src/Pure/Thy/present.ML Tue Mar 09 12:12:45 1999 +0100
+++ b/src/Pure/Thy/present.ML Tue Mar 09 12:13:11 1999 +0100
@@ -2,34 +2,23 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Theory presentation. (* FIXME fake implementation *)
+Theory presentation abstract interface.
+
+TODO:
+ - presentation_modes: AND (!?);
*)
signature BASIC_PRESENT =
sig
- val section: string -> unit
+ include BASIC_BROWSER_INFO
end;
signature PRESENT =
sig
- include BASIC_PRESENT
- val init: bool -> string list -> string list -> string -> string -> unit
- val finish: unit -> unit
- val theory_file: string -> string -> unit
- val thm: string -> thm -> unit
+ include BROWSER_INFO
end;
-structure Present: PRESENT =
-struct
-
-fun init _ _ _ _ _ = ();
-fun finish _ = ();
-
-fun section _ = ();
-fun theory_file _ _ = ();
-fun thm _ _ = ();
-
-end;
+structure Present: PRESENT = BrowserInfo; (* FIXME *)
structure BasicPresent: BASIC_PRESENT = Present;
open BasicPresent;