src/Pure/Thy/present.ML

     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Theory presentation: HTML, graph files, (PDF)LaTeX documents.
 *)
 
-signature BASIC_PRESENT =
-sig
-  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
-end;
-
 signature PRESENT =
 sig
-  include BASIC_PRESENT
   val session_name: theory -> string
+  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
   val read_variant: string -> string * string
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
   val init_theory: string -> unit

     Isabelle_System.isabelle_tool "display" ("-c " ^ File.shell_path detachable_result ^ " &")
   end);
 
 end;
 
-structure Basic_Present: BASIC_PRESENT = Present;
-open Basic_Present;