still fake, passes BrowserInfo;
authorwenzelm
Tue, 09 Mar 1999 12:13:11 +0100
changeset 6325 2822885f5e02
parent 6324 3b7111b360b1
child 6326 1b55802e2b59
still fake, passes BrowserInfo;
src/Pure/Thy/present.ML
--- 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;