27 val preference_real: category -> string option -> |
27 val preference_real: category -> string option -> |
28 real Unsynchronized.ref -> string -> string -> unit |
28 real Unsynchronized.ref -> string -> string -> unit |
29 val preference_string: category -> string option -> |
29 val preference_string: category -> string option -> |
30 string Unsynchronized.ref -> string -> string -> unit |
30 string Unsynchronized.ref -> string -> string -> unit |
31 val preference_option: category -> string option -> string -> string -> string -> unit |
31 val preference_option: category -> string option -> string -> string -> string -> unit |
|
32 val process_pgip: string -> unit |
|
33 val tell_clear_goals: unit -> unit |
|
34 val tell_clear_response: unit -> unit |
|
35 val inform_file_processed: string -> unit |
|
36 val inform_file_retracted: string -> unit |
32 structure ThyLoad: sig val add_path: string -> unit end |
37 structure ThyLoad: sig val add_path: string -> unit end |
33 val thm_deps: bool Unsynchronized.ref |
38 val thm_deps: bool Unsynchronized.ref |
34 val proof_generalN: string |
39 val proof_generalN: string |
35 val init: unit -> unit |
40 val init: unit -> unit |
|
41 val restart: unit -> unit |
36 end; |
42 end; |
37 |
43 |
38 structure ProofGeneral: PROOF_GENERAL = |
44 structure ProofGeneral: PROOF_GENERAL = |
39 struct |
45 struct |
40 |
46 |
424 tell_clear_goals (); |
430 tell_clear_goals (); |
425 tell_clear_response (); |
431 tell_clear_response (); |
426 Isar.init (); |
432 Isar.init (); |
427 welcome ()); |
433 welcome ()); |
428 |
434 |
429 |
435 end; |
430 |
436 |
431 (** Isar command syntax **) |
|
432 |
|
433 val _ = |
|
434 Outer_Syntax.improper_command |
|
435 (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)" |
|
436 (Parse.text >> (fn str => Toplevel.imperative (fn () => process_pgip str))); |
|
437 |
|
438 val _ = |
|
439 Outer_Syntax.improper_command |
|
440 (("ProofGeneral.pr", Keyword.diag), Position.none) "print state (internal)" |
|
441 (Scan.succeed (Toplevel.keep (fn state => |
|
442 if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals () |
|
443 else (Toplevel.quiet := false; Toplevel.print_state true state)))); |
|
444 |
|
445 val _ = (*undo without output -- historical*) |
|
446 Outer_Syntax.improper_command |
|
447 (("ProofGeneral.undo", Keyword.control), Position.none) "(internal)" |
|
448 (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1))); |
|
449 |
|
450 val _ = |
|
451 Outer_Syntax.improper_command |
|
452 (("ProofGeneral.restart", Keyword.control), Position.none) "(internal)" |
|
453 (Parse.opt_unit >> (K (Toplevel.imperative restart))); |
|
454 |
|
455 val _ = |
|
456 Outer_Syntax.improper_command |
|
457 (("ProofGeneral.kill_proof", Keyword.control), Position.none) "(internal)" |
|
458 (Scan.succeed (Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ())))); |
|
459 |
|
460 val _ = |
|
461 Outer_Syntax.improper_command |
|
462 (("ProofGeneral.inform_file_processed", Keyword.control), Position.none) "(internal)" |
|
463 (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_processed file))); |
|
464 |
|
465 val _ = |
|
466 Outer_Syntax.improper_command |
|
467 (("ProofGeneral.inform_file_retracted", Keyword.control), Position.none) "(internal)" |
|
468 (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file))); |
|
469 |
|
470 end; |
|
471 |
|