79 val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit |
79 val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit |
80 val qed_goalw: string -> theory->thm list->string->(thm list->tactic list) |
80 val qed_goalw: string -> theory->thm list->string->(thm list->tactic list) |
81 -> unit |
81 -> unit |
82 val get_thm : theory -> string -> thm |
82 val get_thm : theory -> string -> thm |
83 val thms_of : theory -> (string * thm) list |
83 val thms_of : theory -> (string * thm) list |
|
84 val delete_thms : string -> unit |
84 |
85 |
85 val add_thydata : theory -> string * thy_methods -> unit |
86 val add_thydata : theory -> string * thy_methods -> unit |
86 val get_thydata : theory -> string -> exn option |
87 val get_thydata : theory -> string -> exn option |
87 val add_thy_reader_file: string -> unit |
88 val add_thy_reader_file: string -> unit |
88 val set_thy_reader_file: string -> unit |
89 val set_thy_reader_file: string -> unit |
340 else |
341 else |
341 let val ThyInfo {thy_time, ml_time, ...} = the t |
342 let val ThyInfo {thy_time, ml_time, ...} = the t |
342 in set_info tname (if is_none thy_time then None else Some "") |
343 in set_info tname (if is_none thy_time then None else Some "") |
343 (if is_none ml_time then None else Some "") |
344 (if is_none ml_time then None else Some "") |
344 end |
345 end |
|
346 end; |
|
347 |
|
348 (*Remove theorems associated with a theory from theory and theorem database*) |
|
349 fun delete_thms tname = |
|
350 let |
|
351 val tinfo = case get_thyinfo tname of |
|
352 Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, |
|
353 methods, data, ...}) => |
|
354 ThyInfo {path = path, children = children, parents = parents, |
|
355 thy_time = thy_time, ml_time = ml_time, |
|
356 theory = theory, thms = Symtab.null, |
|
357 methods = methods, data = data} |
|
358 | None => ThyInfo {path = "", children = [], parents = [], |
|
359 thy_time = None, ml_time = None, |
|
360 theory = None, thms = Symtab.null, |
|
361 methods = Symtab.null, |
|
362 data = (Symtab.null, Symtab.null)}; |
|
363 |
|
364 val ThyInfo {theory, ...} = tinfo; |
|
365 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); |
|
366 case theory of |
|
367 Some t => delete_thm_db t |
|
368 | None => () |
345 end; |
369 end; |
346 |
370 |
347 (*Make head of HTML dependency charts |
371 (*Make head of HTML dependency charts |
348 Parameters are: |
372 Parameters are: |
349 file: HTML file |
373 file: HTML file |
586 writeln ("The following children of theory " ^ (quote thy) |
610 writeln ("The following children of theory " ^ (quote thy) |
587 ^ " are now out-of-date: " |
611 ^ " are now out-of-date: " |
588 ^ (quote (space_implode "\",\"" loaded))) |
612 ^ (quote (space_implode "\",\"" loaded))) |
589 else (); |
613 else (); |
590 seq mark_outdated present |
614 seq mark_outdated present |
591 end; |
|
592 |
|
593 (*Remove theorems associated with a theory*) |
|
594 fun delete_thms () = |
|
595 let |
|
596 val tinfo = case get_thyinfo tname of |
|
597 Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, |
|
598 methods, data, ...}) => |
|
599 ThyInfo {path = path, children = children, parents = parents, |
|
600 thy_time = thy_time, ml_time = ml_time, |
|
601 theory = theory, thms = Symtab.null, |
|
602 methods = methods, data = data} |
|
603 | None => ThyInfo {path = "", children = [], parents = [], |
|
604 thy_time = None, ml_time = None, |
|
605 theory = None, thms = Symtab.null, |
|
606 methods = Symtab.null, |
|
607 data = (Symtab.null, Symtab.null)}; |
|
608 |
|
609 val ThyInfo {theory, ...} = tinfo; |
|
610 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); |
|
611 case theory of |
|
612 Some t => delete_thm_db t |
|
613 | None => () |
|
614 end; |
615 end; |
615 |
616 |
616 (*Invoke every get method stored in the methods table and store result in |
617 (*Invoke every get method stored in the methods table and store result in |
617 data table*) |
618 data table*) |
618 fun save_data thy_only = |
619 fun save_data thy_only = |
700 let val ThyInfo {methods, data, ...} = the (get_thyinfo tname) |
701 let val ThyInfo {methods, data, ...} = the (get_thyinfo tname) |
701 in init_data methods (Symtab.dest (fst data)) end |
702 in init_data methods (Symtab.dest (fst data)) end |
702 else |
703 else |
703 (writeln ("Reading \"" ^ name ^ ".thy\""); |
704 (writeln ("Reading \"" ^ name ^ ".thy\""); |
704 |
705 |
705 delete_thms (); |
706 delete_thms tname; |
706 read_thy tname thy_file; |
707 read_thy tname thy_file; |
707 use (out_name tname); |
708 use (out_name tname); |
708 save_data true; |
709 save_data true; |
709 |
710 |
710 (*Store axioms of theory |
711 (*Store axioms of theory |