1signature Logging =
2sig
3
4datatype OTDirective = DeleteConstant | DeleteType | SkipThm | DeleteProof
5
6val raw_start_logging : (OTDirective * string) list -> TextIO.outstream -> unit
7val start_logging : string -> unit
8val export_thm    : Thm.thm -> Thm.thm
9val stop_logging  : unit -> unit
10
11type thy_tyop  = OpenTheoryMap.thy_tyop
12type thy_const = OpenTheoryMap.thy_const
13type otname    = OpenTheoryMap.otname
14
15  val set_tyop_name_handler    : (thy_tyop -> otname) -> unit
16  val reset_tyop_name_handler  : unit -> unit
17  val set_const_name_handler   : (thy_const -> otname) -> unit
18  val reset_const_name_handler : unit -> unit
19
20val read_otdfile : string -> (OTDirective * string) list
21
22(*
23[start_logging()] creates a new article file based on the current theory name.
24Calls to [export_thm] that aren't between a call to [start_logging] and a call
25to [stop_logging] won't write anything.
26[raw_start_logging out] is like [start_logging()] but will write the article to the stream [out] rather than a file based on the theory name.
27
28[stop_logging()] finishes writing and closes the article file currently being
29logged.
30
31[export_thm th] writes article commands to make the virtual machine prove,
32remember (in the dictionary), and export the theorem [th]. It should be called
33on all theorems intended to be an article export.
34
35[set_tyop_name_handler h] installs h as the function used to create an OpenTheory name from a HOL4 type operator name when the OpenTheoryMap does not already have a mapping for the HOL4 name.
36[set_const_name_handler h] is similar, for constants.
37[reset_tyop_name_handler()] and [reset_const_name_handler()] remove these custom functions (reverting to the default behaviour of raising an exception when a mapping does not exist).
38*)
39
40end
41