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