# HG changeset patch
# User wenzelm
# Date 920977991 -3600
# Node ID 2822885f5e02515eeb953aee6ca394790d081d6d
# Parent  3b7111b360b1d073210dbf7cdd9e1902b9274150
still fake, passes BrowserInfo;

diff -r 3b7111b360b1 -r 2822885f5e02 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;