author | wenzelm |
Wed, 31 May 2000 14:29:42 +0200 | |
changeset 9010 | ce78dc5e1a73 |
parent 9009 | 20e132267a83 |
child 9011 | 0cfc347f8d19 |
--- a/src/Provers/classical.ML Wed May 31 14:29:29 2000 +0200 +++ b/src/Provers/classical.ML Wed May 31 14:29:42 2000 +0200 @@ -1188,8 +1188,8 @@ val print_clasetP = OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" OuterSyntax.Keyword.diag - (Scan.succeed (Toplevel.keep - (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))); + (Scan.succeed (Toplevel.no_timing o (Toplevel.keep + (Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); val _ = OuterSyntax.add_parsers [print_clasetP];
--- a/src/Provers/simplifier.ML Wed May 31 14:29:29 2000 +0200 +++ b/src/Provers/simplifier.ML Wed May 31 14:29:42 2000 +0200 @@ -551,8 +551,8 @@ val print_simpsetP = OuterSyntax.improper_command "print_simpset" "print context of Simplifier" OuterSyntax.Keyword.diag - (Scan.succeed (Toplevel.keep - (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of)))); + (Scan.succeed (Toplevel.no_timing o (Toplevel.keep + (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of))))); val _ = OuterSyntax.add_parsers [print_simpsetP];
--- a/src/Pure/Interface/proof_general.ML Wed May 31 14:29:29 2000 +0200 +++ b/src/Pure/Interface/proof_general.ML Wed May 31 14:29:42 2000 +0200 @@ -208,35 +208,38 @@ val old_undoP = (* FIXME same name for compatibility with PG/Isabelle99 *) OuterSyntax.improper_command "undo" "undo last command (no output)" K.control - (Scan.succeed IsarCmd.undo); + (Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); val undoP = OuterSyntax.improper_command "ProofGeneral.undo" "undo last command (no output)" K.control - (Scan.succeed IsarCmd.undo); + (Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); val context_thy_onlyP = OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control - (P.name >> IsarThy.init_context update_thy_only); + (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only)); val try_context_thy_onlyP = OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control - (P.name >> (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)); + (P.name >> (Toplevel.no_timing oo + (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only))); val restartP = OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control - (P.opt_unit >> K (Toplevel.imperative isar_restart)); + (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart))); val kill_proofP = OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control - (Scan.succeed (IsarCmd.kill_proof_notify tell_clear_goals)); + (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals)); val inform_file_processedP = OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control - (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_processed name))); + (P.name >> (Toplevel.no_timing oo + (fn name => Toplevel.imperative (fn () => inform_file_processed name)))); val inform_file_retractedP = OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control - (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name))); + (P.name >> (Toplevel.no_timing oo + (fn name => Toplevel.imperative (fn () => inform_file_retracted name)))); fun init_outer_syntax () = OuterSyntax.add_parsers [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
--- a/src/Pure/Isar/isar_syn.ML Wed May 31 14:29:29 2000 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed May 31 14:29:42 2000 +0200 @@ -208,7 +208,7 @@ val useP = OuterSyntax.command "use" "eval ML text from file" K.diag - (P.name >> IsarCmd.use); + (P.name >> (Toplevel.no_timing oo IsarCmd.use)); val mlP = OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag @@ -451,27 +451,27 @@ val cannot_undoP = OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control - (P.name >> IsarCmd.cannot_undo); + (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo)); val clear_undosP = OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control - (P.nat >> IsarCmd.clear_undos_theory); + (P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory)); val redoP = OuterSyntax.improper_command "redo" "redo last command" K.control - (Scan.succeed (Toplevel.print o IsarCmd.redo)); + (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo)); val undos_proofP = OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control - (P.nat >> (Toplevel.print oo IsarCmd.undos_proof)); + (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof)); val undoP = OuterSyntax.improper_command "undo" "undo last command" K.control - (Scan.succeed (Toplevel.print o IsarCmd.undo)); + (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo)); val killP = OuterSyntax.improper_command "kill" "kill current history node" K.control - (Scan.succeed (Toplevel.print o IsarCmd.kill)); + (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill)); @@ -482,67 +482,67 @@ val pretty_setmarginP = OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" - K.diag (P.nat >> IsarCmd.pretty_setmargin); + K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); val print_commandsP = OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag - (Scan.succeed OuterSyntax.print_help); + (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_help)); val print_contextP = OuterSyntax.improper_command "print_context" "print theory context name" K.diag - (Scan.succeed IsarCmd.print_context); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); val print_theoryP = OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag - (Scan.succeed IsarCmd.print_theory); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theory)); val print_syntaxP = OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag - (Scan.succeed IsarCmd.print_syntax); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); val print_theoremsP = OuterSyntax.improper_command "print_theorems" "print theorems known in this theory" K.diag - (Scan.succeed IsarCmd.print_theorems); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); val print_attributesP = OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag - (Scan.succeed IsarCmd.print_attributes); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); val print_methodsP = OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag - (Scan.succeed IsarCmd.print_methods); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); val thms_containingP = OuterSyntax.improper_command "thms_containing" "print theorems containing all given constants" - K.diag (Scan.repeat P.xname >> IsarCmd.print_thms_containing); + K.diag (Scan.repeat P.xname >> (Toplevel.no_timing oo IsarCmd.print_thms_containing)); val print_bindsP = OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag - (Scan.succeed IsarCmd.print_binds); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); val print_lthmsP = OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag - (Scan.succeed IsarCmd.print_lthms); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_lthms)); val print_casesP = OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag - (Scan.succeed IsarCmd.print_cases); + (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); val print_thmsP = OuterSyntax.improper_command "thm" "print theorems" K.diag - (opt_modes -- P.xthms1 >> IsarCmd.print_thms); + (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); val print_propP = OuterSyntax.improper_command "prop" "read and print proposition" K.diag - (opt_modes -- P.term >> IsarCmd.print_prop); + (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); val print_termP = OuterSyntax.improper_command "term" "read and print term" K.diag - (opt_modes -- P.term >> IsarCmd.print_term); + (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); val print_typeP = OuterSyntax.improper_command "typ" "read and print type" K.diag - (opt_modes -- P.typ >> IsarCmd.print_type); + (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); @@ -550,79 +550,79 @@ val cdP = OuterSyntax.improper_command "cd" "change current working directory" K.diag - (P.name >> IsarCmd.cd); + (P.name >> (Toplevel.no_timing oo IsarCmd.cd)); val pwdP = OuterSyntax.improper_command "pwd" "print current working directory" K.diag - (Scan.succeed IsarCmd.pwd); + (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); val use_thyP = OuterSyntax.improper_command "use_thy" "use theory file" K.diag - (P.name >> IsarCmd.use_thy); + (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy)); val use_thy_onlyP = OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" - K.diag (P.name >> IsarCmd.use_thy_only); + K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only)); val update_thyP = OuterSyntax.improper_command "update_thy" "update theory file" K.diag - (P.name >> IsarCmd.update_thy); + (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy)); val update_thy_onlyP = OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML" - K.diag (P.name >> IsarCmd.update_thy_only); + K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only)); val touch_thyP = OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag - (P.name >> IsarCmd.touch_thy); + (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy)); val touch_all_thysP = OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag - (Scan.succeed IsarCmd.touch_all_thys); + (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys)); val touch_child_thysP = OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag - (P.name >> IsarCmd.touch_child_thys); + (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys)); val remove_thyP = OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag - (P.name >> IsarCmd.remove_thy); + (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy)); val kill_thyP = OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database" - K.diag (P.name >> IsarCmd.kill_thy); + K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy)); val prP = OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag - (opt_modes -- Scan.option P.nat >> IsarCmd.pr); + (opt_modes -- Scan.option P.nat >> (Toplevel.no_timing oo IsarCmd.pr)); val disable_prP = OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag - (Scan.succeed IsarCmd.disable_pr); + (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); val enable_prP = OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag - (Scan.succeed IsarCmd.enable_pr); + (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); val commitP = OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag - (P.opt_unit >> (K IsarCmd.use_commit)); + (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit)); val quitP = OuterSyntax.improper_command "quit" "quit Isabelle" K.control - (P.opt_unit >> (K IsarCmd.quit)); + (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); val exitP = OuterSyntax.improper_command "exit" "exit Isar loop" K.control - (Scan.succeed IsarCmd.exit); + (Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); val init_toplevelP = OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control - (Scan.succeed IsarCmd.init_toplevel); + (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel)); val welcomeP = OuterSyntax.improper_command "welcome" "print welcome message" K.diag - (Scan.succeed IsarCmd.welcome); + (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
--- a/src/Pure/Isar/toplevel.ML Wed May 31 14:29:29 2000 +0200 +++ b/src/Pure/Isar/toplevel.ML Wed May 31 14:29:42 2000 +0200 @@ -35,6 +35,7 @@ val position: Position.T -> transition -> transition val interactive: bool -> transition -> transition val print: transition -> transition + val no_timing: transition -> transition val reset: transition -> transition val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition val exit: transition -> transition @@ -272,15 +273,17 @@ pos: Position.T, int_only: bool, print: bool, + no_timing: bool, trans: trans list}; -fun make_transition (name, pos, int_only, print, trans) = - Transition {name = name, pos = pos, int_only = int_only, print = print, trans = trans}; +fun make_transition (name, pos, int_only, print, no_timing, trans) = + Transition {name = name, pos = pos, int_only = int_only, print = print, + no_timing = no_timing, trans = trans}; -fun map_transition f (Transition {name, pos, int_only, print, trans}) = - make_transition (f (name, pos, int_only, print, trans)); +fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) = + make_transition (f (name, pos, int_only, print, no_timing, trans)); -val empty = make_transition ("<unknown>", Position.none, false, false, []); +val empty = make_transition ("<unknown>", Position.none, false, false, false, []); (* diagnostics *) @@ -296,20 +299,23 @@ (* modify transitions *) -fun name nm = map_transition - (fn (_, pos, int_only, print, trans) => (nm, pos, int_only, print, trans)); +fun name nm = map_transition (fn (_, pos, int_only, print, no_timing, trans) => + (nm, pos, int_only, print, no_timing, trans)); -fun position pos = map_transition - (fn (name, _, int_only, print, trans) => (name, pos, int_only, print, trans)); +fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) => + (name, pos, int_only, print, no_timing, trans)); + +fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) => + (name, pos, int_only, print, no_timing, trans)); -fun interactive int_only = map_transition - (fn (name, pos, _, print, trans) => (name, pos, int_only, print, trans)); +val print = map_transition (fn (name, pos, int_only, _, no_timing, trans) => + (name, pos, int_only, true, no_timing, trans)); -val print = map_transition - (fn (name, pos, int_only, _, trans) => (name, pos, int_only, true, trans)); +val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) => + (name, pos, int_only, print, true, trans)); -fun add_trans tr = map_transition - (fn (name, pos, int_only, print, trans) => (name, pos, int_only, print, trans @ [tr])); +fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) => + (name, pos, int_only, print, no_timing, trans @ [tr])); (* build transitions *) @@ -381,13 +387,14 @@ local -fun app int (tr as Transition {trans, int_only, print, ...}) state = +fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state = let val _ = if int orelse not int_only then () else warning (command_msg "Interactive-only " tr); val (result, opt_exn) = - (if ! Library.timing then (warning (command_msg "" tr); timeap) else I) (apply_trans int trans) state; + (if ! Library.timing andalso not no_timing then (warning (command_msg "" tr); timeap) else I) + (apply_trans int trans) state; val _ = if int andalso print andalso not (! quiet) then print_state false result else (); in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;