src/Pure/Isar/toplevel.ML
author wenzelm
Tue, 05 Jul 2011 19:45:59 +0200
changeset 43667 6d73cceb1503
parent 43665 573d1272f36d
child 43668 aad4f1956098
permissions -rw-r--r--
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example); reduced Theory.end_theory to plain projection, outside transaction context (see also ddc3b72f9a42);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/toplevel.ML
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
     3
26602
5534b6a6b810 made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents: 26491
diff changeset
     4
Isabelle/Isar toplevel transactions.
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
     5
*)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
     6
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
     7
signature TOPLEVEL =
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
     8
sig
19063
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
     9
  exception UNDEF
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    10
  type state
26602
5534b6a6b810 made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents: 26491
diff changeset
    11
  val toplevel: state
7732
d62523296573 added is_toplevel;
wenzelm
parents: 7612
diff changeset
    12
  val is_toplevel: state -> bool
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
    13
  val is_theory: state -> bool
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
    14
  val is_proof: state -> bool
17076
c7effdf2e2e2 state: body context;
wenzelm
parents: 16815
diff changeset
    15
  val level: state -> int
30398
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
    16
  val presentation_context_of: state -> Proof.context
30801
9bdf001bea58 added Toplevel.previous_node_of;
wenzelm
parents: 30618
diff changeset
    17
  val previous_context_of: state -> Proof.context option
21506
b2a673894ce5 prefer Proof.context over Context.generic;
wenzelm
parents: 21310
diff changeset
    18
  val context_of: state -> Proof.context
22089
d9b614dc883d added generic_theory_of;
wenzelm
parents: 22056
diff changeset
    19
  val generic_theory_of: state -> generic_theory
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    20
  val theory_of: state -> theory
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    21
  val proof_of: state -> Proof.state
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
    22
  val proof_position_of: state -> int
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
    23
  val end_theory: Position.T -> state -> theory
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
    24
  val print_state_context: state -> unit
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
    25
  val print_state: bool -> state -> unit
37858
e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state;
wenzelm
parents: 37856
diff changeset
    26
  val pretty_abstract: state -> Pretty.T
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    27
  val quiet: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    28
  val debug: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    29
  val interact: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    30
  val timing: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    31
  val profiling: int Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    32
  val skip_proofs: bool Unsynchronized.ref
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
    33
  val program: (unit -> 'a) -> 'a
33604
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
    34
  val thread: bool -> (unit -> unit) -> Thread.thread
16682
wenzelm
parents: 16658
diff changeset
    35
  type transition
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    36
  val empty: transition
27441
38ccd5aaa353 init_theory: pass name explicitly;
wenzelm
parents: 27427
diff changeset
    37
  val init_of: transition -> string option
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
    38
  val print_of: transition -> bool
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
    39
  val name_of: transition -> string
28105
44054657ea56 added pos_of;
wenzelm
parents: 28103
diff changeset
    40
  val pos_of: transition -> Position.T
27500
f1c18ec9f2d7 export str_of;
wenzelm
parents: 27441
diff changeset
    41
  val str_of: transition -> string
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    42
  val name: string -> transition -> transition
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    43
  val position: Position.T -> transition -> transition
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    44
  val interactive: bool -> transition -> transition
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
    45
  val set_print: bool -> transition -> transition
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    46
  val print: transition -> transition
9010
ce78dc5e1a73 Toplevel.no_timing;
wenzelm
parents: 8999
diff changeset
    47
  val no_timing: transition -> transition
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
    48
  val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
    49
  val modify_master: Path.T option -> transition -> transition
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
    50
  val modify_init: (Path.T option -> theory) -> transition -> transition
6689
wenzelm
parents: 6664
diff changeset
    51
  val exit: transition -> transition
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    52
  val keep: (state -> unit) -> transition -> transition
7612
ba11b5db431a added keep', theory';
wenzelm
parents: 7602
diff changeset
    53
  val keep': (bool -> state -> unit) -> transition -> transition
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    54
  val imperative: (unit -> unit) -> transition -> transition
27840
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
    55
  val ignored: Position.T -> transition
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
    56
  val malformed: Position.T -> string -> transition
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    57
  val theory: (theory -> theory) -> transition -> transition
26491
c93ff30790fe added generic_theory transaction;
wenzelm
parents: 26293
diff changeset
    58
  val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
7612
ba11b5db431a added keep', theory';
wenzelm
parents: 7602
diff changeset
    59
  val theory': (bool -> theory -> theory) -> transition -> transition
20985
de13e2a23c8e exit_local_theory: pass interactive flag;
wenzelm
parents: 20963
diff changeset
    60
  val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
    61
  val end_local_theory: transition -> transition
29380
a9ee3475abf4 added local_theory';
wenzelm
parents: 29343
diff changeset
    62
  val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
a9ee3475abf4 added local_theory';
wenzelm
parents: 29343
diff changeset
    63
    transition -> transition
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
    64
  val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
    65
  val present_local_theory: xstring option -> (state -> unit) -> transition -> transition
24453
86cf57ddf8f6 Added local_theory_to_proof'
berghofe
parents: 24295
diff changeset
    66
  val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
86cf57ddf8f6 Added local_theory_to_proof'
berghofe
parents: 24295
diff changeset
    67
    transition -> transition
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
    68
  val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
    69
    transition -> transition
17363
046c829c075f added three_buffersN, print3;
wenzelm
parents: 17321
diff changeset
    70
  val theory_to_proof: (theory -> Proof.state) -> transition -> transition
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
    71
  val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
    72
  val forget_proof: transition -> transition
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
    73
  val present_proof: (state -> unit) -> transition -> transition
21177
e8228486aa03 removed checkpoint interface;
wenzelm
parents: 21007
diff changeset
    74
  val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
17904
21c6894b5998 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents: 17513
diff changeset
    75
  val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
21177
e8228486aa03 removed checkpoint interface;
wenzelm
parents: 21007
diff changeset
    76
  val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
e8228486aa03 removed checkpoint interface;
wenzelm
parents: 21007
diff changeset
    77
  val proof: (Proof.state -> Proof.state) -> transition -> transition
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
    78
  val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
    79
  val skip_proof: (int -> int) -> transition -> transition
17904
21c6894b5998 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents: 17513
diff changeset
    80
  val skip_proof_to_theory: (int -> bool) -> transition -> transition
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
    81
  val get_id: transition -> string option
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
    82
  val put_id: string -> transition -> transition
9512
c30f6d0f81d2 added unknown_theory/proof/context;
wenzelm
parents: 9453
diff changeset
    83
  val unknown_theory: transition -> transition
c30f6d0f81d2 added unknown_theory/proof/context;
wenzelm
parents: 9453
diff changeset
    84
  val unknown_proof: transition -> transition
c30f6d0f81d2 added unknown_theory/proof/context;
wenzelm
parents: 9453
diff changeset
    85
  val unknown_context: transition -> transition
28425
25d6099179a6 export setmp_thread_position;
wenzelm
parents: 28394
diff changeset
    86
  val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27603
diff changeset
    87
  val status: transition -> Markup.T -> unit
38876
ec7045139e70 Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents: 38875
diff changeset
    88
  val error_msg: transition -> string -> unit
28103
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28095
diff changeset
    89
  val add_hook: (transition -> state -> state -> unit) -> unit
26602
5534b6a6b810 made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents: 26491
diff changeset
    90
  val transition: bool -> transition -> state -> (state * (exn * string) option) option
28425
25d6099179a6 export setmp_thread_position;
wenzelm
parents: 28394
diff changeset
    91
  val command: transition -> state -> state
42129
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
    92
  val excursion:
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
    93
    (transition * transition list) list -> (transition * state) list future list * theory
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    94
end;
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    95
6965
a766de752996 fixed interrupts (eliminated races);
wenzelm
parents: 6689
diff changeset
    96
structure Toplevel: TOPLEVEL =
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    97
struct
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    98
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    99
(** toplevel state **)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   100
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   101
exception UNDEF = Runtime.UNDEF;
19063
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
   102
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
   103
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   104
(* local theory wrappers *)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   105
38350
480b2de9927c renamed Theory_Target to the more appropriate Named_Target
haftmann
parents: 38236
diff changeset
   106
val loc_init = Named_Target.context_cmd;
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33604
diff changeset
   107
val loc_exit = Local_Theory.exit_global;
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   108
25292
f082e59551b0 simplified LocalTheory.reinit;
wenzelm
parents: 25269
diff changeset
   109
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   110
  | loc_begin NONE (Context.Proof lthy) = lthy
38391
ba1cc1815ce1 named target is optional; explicit Name_Target.reinit
haftmann
parents: 38389
diff changeset
   111
  | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy;
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   112
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   113
fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33604
diff changeset
   114
  | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
38391
ba1cc1815ce1 named target is optional; explicit Name_Target.reinit
haftmann
parents: 38389
diff changeset
   115
  | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy;
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   116
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   117
21958
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   118
(* datatype node *)
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   119
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   120
datatype node =
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   121
  Theory of generic_theory * Proof.context option
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   122
    (*theory with presentation context*) |
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   123
  Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   124
    (*proof node, finish, original theory*) |
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   125
  SkipProof of int * (generic_theory * generic_theory);
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   126
    (*proof depth, resulting theory, original theory*)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   127
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   128
val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   129
val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   130
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   131
fun cases_node f _ (Theory (gthy, _)) = f gthy
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   132
  | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   133
  | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
19063
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
   134
29066
f50c24e5b9fe export context_node;
wenzelm
parents: 28999
diff changeset
   135
val context_node = cases_node Context.proof_of Proof.context_of;
f50c24e5b9fe export context_node;
wenzelm
parents: 28999
diff changeset
   136
21958
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   137
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   138
(* datatype state *)
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   139
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   140
datatype state = State of node option * node option;  (*current, previous*)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   141
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   142
val toplevel = State (NONE, NONE);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   143
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   144
fun is_toplevel (State (NONE, _)) = true
7732
d62523296573 added is_toplevel;
wenzelm
parents: 7612
diff changeset
   145
  | is_toplevel _ = false;
d62523296573 added is_toplevel;
wenzelm
parents: 7612
diff changeset
   146
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   147
fun level (State (NONE, _)) = 0
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   148
  | level (State (SOME (Theory _), _)) = 0
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   149
  | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   150
  | level (State (SOME (SkipProof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
17076
c7effdf2e2e2 state: body context;
wenzelm
parents: 16815
diff changeset
   151
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   152
fun str_of_state (State (NONE, _)) = "at top level"
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   153
  | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   154
  | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   155
  | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   156
  | str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode";
5946
a4600d21b59b print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents: 5939
diff changeset
   157
a4600d21b59b print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents: 5939
diff changeset
   158
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   159
(* current node *)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   160
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   161
fun node_of (State (NONE, _)) = raise UNDEF
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   162
  | node_of (State (SOME node, _)) = node;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   163
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   164
fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   165
fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   166
19063
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
   167
fun node_case f g state = cases_node f g (node_of state);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   168
30398
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   169
fun presentation_context_of state =
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   170
  (case try node_of state of
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   171
    SOME (Theory (_, SOME ctxt)) => ctxt
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   172
  | SOME node => context_node node
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   173
  | NONE => raise UNDEF);
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   174
30801
9bdf001bea58 added Toplevel.previous_node_of;
wenzelm
parents: 30618
diff changeset
   175
fun previous_context_of (State (_, NONE)) = NONE
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   176
  | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
30801
9bdf001bea58 added Toplevel.previous_node_of;
wenzelm
parents: 30618
diff changeset
   177
21506
b2a673894ce5 prefer Proof.context over Context.generic;
wenzelm
parents: 21310
diff changeset
   178
val context_of = node_case Context.proof_of Proof.context_of;
22089
d9b614dc883d added generic_theory_of;
wenzelm
parents: 22056
diff changeset
   179
val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   180
val theory_of = node_case Context.theory_of Proof.theory_of;
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   181
val proof_of = node_case (fn _ => raise UNDEF) I;
17208
49bc1bdc7b6e added no_body_context;
wenzelm
parents: 17115
diff changeset
   182
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   183
fun proof_position_of state =
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   184
  (case node_of state of
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   185
    Proof (prf, _) => Proof_Node.position prf
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   186
  | _ => raise UNDEF);
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   187
43667
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   188
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   189
  | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   190
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   191
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   192
(* print state *)
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   193
38388
94d5624dd1f7 Named_Target.theory_init
haftmann
parents: 38384
diff changeset
   194
val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   195
23640
baec2e674461 toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23619
diff changeset
   196
fun print_state_context state =
24795
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   197
  (case try node_of state of
21506
b2a673894ce5 prefer Proof.context over Context.generic;
wenzelm
parents: 21310
diff changeset
   198
    NONE => []
24795
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   199
  | SOME (Theory (gthy, _)) => pretty_context gthy
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   200
  | SOME (Proof (_, (_, gthy))) => pretty_context gthy
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   201
  | SOME (SkipProof (_, (gthy, _))) => pretty_context gthy)
23640
baec2e674461 toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23619
diff changeset
   202
  |> Pretty.chunks |> Pretty.writeln;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   203
23640
baec2e674461 toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23619
diff changeset
   204
fun print_state prf_only state =
23701
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   205
  (case try node_of state of
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   206
    NONE => []
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   207
  | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   208
  | SOME (Proof (prf, _)) =>
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   209
      Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   210
  | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
23701
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   211
  |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   212
37858
e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state;
wenzelm
parents: 37856
diff changeset
   213
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state;
wenzelm
parents: 37856
diff changeset
   214
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   215
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   216
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   217
(** toplevel transitions **)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   218
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   219
val quiet = Unsynchronized.ref false;
39513
fce2202892c4 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents: 39285
diff changeset
   220
val debug = Runtime.debug;
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   221
val interact = Unsynchronized.ref false;
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 41703
diff changeset
   222
val timing = Unsynchronized.ref false;
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   223
val profiling = Unsynchronized.ref 0;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   224
val skip_proofs = Unsynchronized.ref false;
16682
wenzelm
parents: 16658
diff changeset
   225
33604
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   226
fun program body =
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   227
 (body
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   228
  |> Runtime.controlled_execution
33604
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   229
  |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   230
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   231
fun thread interrupts body =
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   232
  Thread.fork
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 38888
diff changeset
   233
    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
33604
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   234
        |> Runtime.debugging
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   235
        |> Runtime.toplevel_error
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39513
diff changeset
   236
          (fn exn =>
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39513
diff changeset
   237
            Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37208
diff changeset
   238
      Simple_Thread.attributes interrupts);
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   239
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   240
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   241
(* node transactions -- maintaining stable checkpoints *)
7022
abf9d5e2fb6e removed BREAK, ROLLBACK;
wenzelm
parents: 6971
diff changeset
   242
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   243
exception FAILURE of state * exn;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   244
6689
wenzelm
parents: 6664
diff changeset
   245
local
wenzelm
parents: 6664
diff changeset
   246
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   247
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   248
  | reset_presentation node = node;
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   249
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   250
fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy)
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   251
  | is_draft_theory _ = false;
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   252
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   253
fun is_stale state = Context.is_stale (theory_of state) handle Runtime.UNDEF => false;
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   254
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   255
fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!")
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   256
  | stale_error some = some;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   257
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   258
fun map_theory f (Theory (gthy, ctxt)) =
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33604
diff changeset
   259
      Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt)
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   260
  | map_theory _ node = node;
6689
wenzelm
parents: 6664
diff changeset
   261
wenzelm
parents: 6664
diff changeset
   262
in
wenzelm
parents: 6664
diff changeset
   263
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   264
fun apply_transaction f g node =
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   265
  let
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   266
    val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   267
    val cont_node = reset_presentation node;
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   268
    val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node;
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   269
    fun state_error e nd = (State (SOME nd, SOME node), e);
6689
wenzelm
parents: 6664
diff changeset
   270
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   271
    val (result, err) =
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   272
      cont_node
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   273
      |> Runtime.controlled_execution f
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   274
      |> map_theory Theory.checkpoint
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   275
      |> state_error NONE
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   276
      handle exn => state_error (SOME exn) cont_node;
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   277
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   278
    val (result', err') =
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   279
      if is_stale result then state_error (stale_error err) back_node
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   280
      else (result, err);
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   281
  in
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   282
    (case err' of
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   283
      NONE => tap g result'
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   284
    | SOME exn => raise FAILURE (result', exn))
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   285
  end;
6689
wenzelm
parents: 6664
diff changeset
   286
43667
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   287
val exit_transaction =
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   288
  apply_transaction
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   289
    (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE)
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   290
      | node => node) (K ())
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   291
  #> (fn State (node', _) => State (NONE, node'));
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   292
6689
wenzelm
parents: 6664
diff changeset
   293
end;
wenzelm
parents: 6664
diff changeset
   294
wenzelm
parents: 6664
diff changeset
   295
wenzelm
parents: 6664
diff changeset
   296
(* primitive transitions *)
wenzelm
parents: 6664
diff changeset
   297
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   298
datatype trans =
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   299
  Init of Path.T option * string * (Path.T option -> theory) | (*master dir, theory name, init*)
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   300
  Exit |                                 (*formal exit of theory*)
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   301
  Keep of bool -> state -> unit |        (*peek at state*)
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   302
  Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
21958
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   303
6689
wenzelm
parents: 6664
diff changeset
   304
local
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   305
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   306
fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
33727
e2d5d7f51aa3 init_theory: Runtime.controlled_execution for proper exception trace etc.;
wenzelm
parents: 33725
diff changeset
   307
      State (SOME (Theory (Context.Theory
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   308
          (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
43667
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   309
  | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
6d73cceb1503 explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents: 43665
diff changeset
   310
      exit_transaction state
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   311
  | apply_tr int (Keep f) state =
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   312
      Runtime.controlled_execution (fn x => tap (f int) x) state
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   313
  | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   314
      apply_transaction (fn x => f int x) g state
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   315
  | apply_tr _ _ _ = raise UNDEF;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   316
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   317
fun apply_union _ [] state = raise FAILURE (state, UNDEF)
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   318
  | apply_union int (tr :: trs) state =
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   319
      apply_union int trs state
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   320
        handle Runtime.UNDEF => apply_tr int tr state
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   321
          | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state
6689
wenzelm
parents: 6664
diff changeset
   322
          | exn as FAILURE _ => raise exn
wenzelm
parents: 6664
diff changeset
   323
          | exn => raise FAILURE (state, exn);
wenzelm
parents: 6664
diff changeset
   324
wenzelm
parents: 6664
diff changeset
   325
in
wenzelm
parents: 6664
diff changeset
   326
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   327
fun apply_trans int trs state = (apply_union int trs state, NONE)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15519
diff changeset
   328
  handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
6689
wenzelm
parents: 6664
diff changeset
   329
wenzelm
parents: 6664
diff changeset
   330
end;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   331
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   332
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   333
(* datatype transition *)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   334
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   335
datatype transition = Transition of
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   336
 {name: string,              (*command name*)
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   337
  pos: Position.T,           (*source position*)
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   338
  int_only: bool,            (*interactive-only*)
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   339
  print: bool,               (*print result state*)
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   340
  no_timing: bool,           (*suppress timing*)
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   341
  trans: trans list};        (*primitive transitions (union)*)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   342
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   343
fun make_transition (name, pos, int_only, print, no_timing, trans) =
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   344
  Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing,
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   345
    trans = trans};
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   346
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   347
fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) =
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   348
  make_transition (f (name, pos, int_only, print, no_timing, trans));
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   349
27441
38ccd5aaa353 init_theory: pass name explicitly;
wenzelm
parents: 27427
diff changeset
   350
val empty = make_transition ("", Position.none, false, false, false, []);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   351
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   352
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   353
(* diagnostics *)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   354
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   355
fun get_init (Transition {trans = [Init args], ...}) = SOME args
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   356
  | get_init _ = NONE;
27441
38ccd5aaa353 init_theory: pass name explicitly;
wenzelm
parents: 27427
diff changeset
   357
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   358
val init_of = Option.map #2 o get_init;
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
   359
fun print_of (Transition {print, ...}) = print;
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   360
fun name_of (Transition {name, ...}) = name;
28105
44054657ea56 added pos_of;
wenzelm
parents: 28103
diff changeset
   361
fun pos_of (Transition {pos, ...}) = pos;
44054657ea56 added pos_of;
wenzelm
parents: 28103
diff changeset
   362
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   363
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   364
fun command_msg msg tr = msg ^ "command " ^ str_of tr;
38875
c7a66b584147 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents: 38721
diff changeset
   365
fun at_command tr = command_msg "At " tr;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   366
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   367
fun type_error tr state =
18685
725660906cb3 sane ERROR vs. TOPLEVEL_ERROR handling;
wenzelm
parents: 18664
diff changeset
   368
  ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   369
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   370
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   371
(* modify transitions *)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   372
28451
0586b855c2b5 datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents: 28446
diff changeset
   373
fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
0586b855c2b5 datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents: 28446
diff changeset
   374
  (name, pos, int_only, print, no_timing, trans));
9010
ce78dc5e1a73 Toplevel.no_timing;
wenzelm
parents: 8999
diff changeset
   375
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   376
fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) =>
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   377
  (name, pos, int_only, print, no_timing, trans));
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   378
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   379
fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) =>
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   380
  (name, pos, int_only, print, no_timing, trans));
14923
8a32071c3c13 added name_of, source_of, source;
wenzelm
parents: 14825
diff changeset
   381
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   382
val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   383
  (name, pos, int_only, print, true, trans));
17363
046c829c075f added three_buffersN, print3;
wenzelm
parents: 17321
diff changeset
   384
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   385
fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) =>
28451
0586b855c2b5 datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents: 28446
diff changeset
   386
  (name, pos, int_only, print, no_timing, tr :: trans));
16607
81e687c63e29 added print': print depending on print_mode;
wenzelm
parents: 16490
diff changeset
   387
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   388
val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) =>
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   389
  (name, pos, int_only, print, no_timing, []));
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   390
28453
06702e7acd1d excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents: 28451
diff changeset
   391
fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
06702e7acd1d excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents: 28451
diff changeset
   392
  (name, pos, int_only, print, no_timing, trans));
06702e7acd1d excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents: 28451
diff changeset
   393
06702e7acd1d excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents: 28451
diff changeset
   394
val print = set_print true;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   395
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   396
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   397
(* basic transitions *)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   398
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   399
fun init_theory master name f = add_trans (Init (master, name, f));
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   400
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   401
fun modify_master master tr =
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   402
  (case get_init tr of
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   403
    SOME (_, name, f) => init_theory master name f (reset_trans tr)
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   404
  | NONE => tr);
37977
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37953
diff changeset
   405
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37953
diff changeset
   406
fun modify_init f tr =
41536
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   407
  (case get_init tr of
47fef6afe756 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm
parents: 40960
diff changeset
   408
    SOME (master, name, _) => init_theory master name f (reset_trans tr)
37977
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37953
diff changeset
   409
  | NONE => tr);
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37953
diff changeset
   410
6689
wenzelm
parents: 6664
diff changeset
   411
val exit = add_trans Exit;
7612
ba11b5db431a added keep', theory';
wenzelm
parents: 7602
diff changeset
   412
val keep' = add_trans o Keep;
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   413
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   414
fun present_transaction f g = add_trans (Transaction (f, g));
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   415
fun transaction f = present_transaction f (K ());
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   416
7612
ba11b5db431a added keep', theory';
wenzelm
parents: 7602
diff changeset
   417
fun keep f = add_trans (Keep (fn _ => f));
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   418
fun imperative f = keep (fn _ => f ());
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   419
27840
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
   420
fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
   421
fun malformed pos msg =
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
   422
  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
   423
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   424
val unknown_theory = imperative (fn () => warning "Unknown theory context");
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   425
val unknown_proof = imperative (fn () => warning "Unknown proof context");
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   426
val unknown_context = imperative (fn () => warning "Unknown context");
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   427
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   428
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   429
(* theory transitions *)
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   430
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   431
fun generic_theory f = transaction (fn _ =>
26491
c93ff30790fe added generic_theory transaction;
wenzelm
parents: 26293
diff changeset
   432
  (fn Theory (gthy, _) => Theory (f gthy, NONE)
c93ff30790fe added generic_theory transaction;
wenzelm
parents: 26293
diff changeset
   433
    | _ => raise UNDEF));
c93ff30790fe added generic_theory transaction;
wenzelm
parents: 26293
diff changeset
   434
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   435
fun theory' f = transaction (fn int =>
33725
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   436
  (fn Theory (Context.Theory thy, _) =>
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   437
      let val thy' = thy
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   438
        |> Sign.new_group
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   439
        |> Theory.checkpoint
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   440
        |> f int
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   441
        |> Sign.reset_group;
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   442
      in Theory (Context.Theory thy', NONE) end
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   443
    | _ => raise UNDEF));
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   444
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   445
fun theory f = theory' (K f);
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   446
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   447
fun begin_local_theory begin f = transaction (fn _ =>
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   448
  (fn Theory (Context.Theory thy, _) =>
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   449
        let
20985
de13e2a23c8e exit_local_theory: pass interactive flag;
wenzelm
parents: 20963
diff changeset
   450
          val lthy = f thy;
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   451
          val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   452
        in Theory (gthy, SOME lthy) end
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   453
    | _ => raise UNDEF));
17076
c7effdf2e2e2 state: body context;
wenzelm
parents: 16815
diff changeset
   454
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   455
val end_local_theory = transaction (fn _ =>
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   456
  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   457
    | _ => raise UNDEF));
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   458
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   459
local
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   460
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   461
fun local_theory_presentation loc f = present_transaction (fn int =>
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   462
  (fn Theory (gthy, _) =>
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   463
        let
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   464
          val finish = loc_finish loc gthy;
33725
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   465
          val lthy' = loc_begin loc gthy
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   466
            |> Local_Theory.new_group
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   467
            |> f int
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   468
            |> Local_Theory.reset_group;
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   469
        in Theory (finish lthy', SOME lthy') end
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   470
    | _ => raise UNDEF));
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   471
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   472
in
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   473
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   474
fun local_theory' loc f = local_theory_presentation loc f (K ());
29380
a9ee3475abf4 added local_theory';
wenzelm
parents: 29343
diff changeset
   475
fun local_theory loc f = local_theory' loc (K f);
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   476
fun present_local_theory loc = local_theory_presentation loc (K I);
18955
fa71f2ddd2e8 added local_theory, with optional locale xname;
wenzelm
parents: 18811
diff changeset
   477
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   478
end;
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   479
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   480
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   481
(* proof transitions *)
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   482
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   483
fun end_proof f = transaction (fn int =>
24795
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   484
  (fn Proof (prf, (finish, _)) =>
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   485
        let val state = Proof_Node.current prf in
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   486
          if can (Proof.assert_bottom true) state then
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   487
            let
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   488
              val ctxt' = f int state;
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   489
              val gthy' = finish ctxt';
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   490
            in Theory (gthy', SOME ctxt') end
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   491
          else raise UNDEF
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   492
        end
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   493
    | SkipProof (0, (gthy, _)) => Theory (gthy, NONE)
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   494
    | _ => raise UNDEF));
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   495
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   496
local
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   497
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   498
fun begin_proof init finish = transaction (fn int =>
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   499
  (fn Theory (gthy, _) =>
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   500
    let
24453
86cf57ddf8f6 Added local_theory_to_proof'
berghofe
parents: 24295
diff changeset
   501
      val prf = init int gthy;
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   502
      val skip = ! skip_proofs;
40960
9e54eb514a46 formal notepad without any result;
wenzelm
parents: 40132
diff changeset
   503
      val (is_goal, no_skip) =
9e54eb514a46 formal notepad without any result;
wenzelm
parents: 40132
diff changeset
   504
        (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   505
    in
40960
9e54eb514a46 formal notepad without any result;
wenzelm
parents: 40132
diff changeset
   506
      if is_goal andalso skip andalso no_skip then
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   507
        warning "Cannot skip proof of schematic goal statement"
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   508
      else ();
40960
9e54eb514a46 formal notepad without any result;
wenzelm
parents: 40132
diff changeset
   509
      if skip andalso not no_skip then
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   510
        SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   511
      else Proof (Proof_Node.init prf, (finish gthy, gthy))
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   512
    end
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   513
  | _ => raise UNDEF));
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   514
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   515
in
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   516
24780
47bb1e380d83 local_theory transactions: more careful treatment of context position;
wenzelm
parents: 24634
diff changeset
   517
fun local_theory_to_proof' loc f = begin_proof
33725
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   518
  (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   519
  (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
24780
47bb1e380d83 local_theory transactions: more careful treatment of context position;
wenzelm
parents: 24634
diff changeset
   520
24453
86cf57ddf8f6 Added local_theory_to_proof'
berghofe
parents: 24295
diff changeset
   521
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   522
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   523
fun theory_to_proof f = begin_proof
33725
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   524
  (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42129
diff changeset
   525
  (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   526
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   527
end;
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   528
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   529
val forget_proof = transaction (fn _ =>
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   530
  (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   531
    | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   532
    | _ => raise UNDEF));
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   533
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   534
val present_proof = present_transaction (fn _ =>
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   535
  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   536
    | skip as SkipProof _ => skip
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   537
    | _ => raise UNDEF));
21177
e8228486aa03 removed checkpoint interface;
wenzelm
parents: 21007
diff changeset
   538
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   539
fun proofs' f = transaction (fn int =>
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   540
  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   541
    | skip as SkipProof _ => skip
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   542
    | _ => raise UNDEF));
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   543
17904
21c6894b5998 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents: 17513
diff changeset
   544
fun proof' f = proofs' (Seq.single oo f);
21c6894b5998 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents: 17513
diff changeset
   545
val proofs = proofs' o K;
6689
wenzelm
parents: 6664
diff changeset
   546
val proof = proof' o K;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   547
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   548
fun actual_proof f = transaction (fn _ =>
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   549
  (fn Proof (prf, x) => Proof (f prf, x)
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   550
    | _ => raise UNDEF));
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   551
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   552
fun skip_proof f = transaction (fn _ =>
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   553
  (fn SkipProof (h, x) => SkipProof (f h, x)
18563
wenzelm
parents: 17904
diff changeset
   554
    | _ => raise UNDEF));
wenzelm
parents: 17904
diff changeset
   555
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   556
fun skip_proof_to_theory pred = transaction (fn _ =>
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   557
  (fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
33725
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   558
    | _ => raise UNDEF));
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   559
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   560
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   561
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   562
(** toplevel transactions **)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   563
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   564
(* identification *)
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   565
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   566
fun get_id (Transition {pos, ...}) = Position.get_id pos;
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   567
fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   568
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   569
25960
1f9956e0bd89 removed unused properties;
wenzelm
parents: 25847
diff changeset
   570
(* thread position *)
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   571
25960
1f9956e0bd89 removed unused properties;
wenzelm
parents: 25847
diff changeset
   572
fun setmp_thread_position (Transition {pos, ...}) f x =
25819
e6feb08b7f4b replaced thread_properties by simplified version in position.ML;
wenzelm
parents: 25809
diff changeset
   573
  Position.setmp_thread_data pos f x;
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   574
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27603
diff changeset
   575
fun status tr m =
43665
573d1272f36d tuned signature;
wenzelm
parents: 42360
diff changeset
   576
  setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27603
diff changeset
   577
38876
ec7045139e70 Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents: 38875
diff changeset
   578
fun error_msg tr msg =
ec7045139e70 Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents: 38875
diff changeset
   579
  setmp_thread_position tr (fn () => Output.error_msg msg) ();
26602
5534b6a6b810 made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents: 26491
diff changeset
   580
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   581
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   582
(* post-transition hooks *)
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   583
37905
wenzelm
parents: 37865
diff changeset
   584
local
wenzelm
parents: 37865
diff changeset
   585
  val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
wenzelm
parents: 37865
diff changeset
   586
in
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   587
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   588
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
33223
d27956b4d3b4 non-critical atomic accesses;
wenzelm
parents: 32792
diff changeset
   589
fun get_hooks () = ! hooks;
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   590
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   591
end;
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   592
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   593
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   594
(* apply transitions *)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   595
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   596
local
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   597
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   598
fun app int (tr as Transition {trans, print, no_timing, ...}) =
25819
e6feb08b7f4b replaced thread_properties by simplified version in position.ML;
wenzelm
parents: 25809
diff changeset
   599
  setmp_thread_position tr (fn state =>
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   600
    let
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   601
      fun do_timing f x = (warning (command_msg "" tr); timeap f x);
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   602
      fun do_profiling f x = profile (! profiling) f x;
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   603
26256
3e7939e978c6 added exception CONTEXT, indicating context of another exception;
wenzelm
parents: 26081
diff changeset
   604
      val (result, status) =
37905
wenzelm
parents: 37865
diff changeset
   605
         state |>
wenzelm
parents: 37865
diff changeset
   606
          (apply_trans int trans
wenzelm
parents: 37865
diff changeset
   607
            |> (! profiling > 0 andalso not no_timing) ? do_profiling
wenzelm
parents: 37865
diff changeset
   608
            |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
26256
3e7939e978c6 added exception CONTEXT, indicating context of another exception;
wenzelm
parents: 26081
diff changeset
   609
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   610
      val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
26256
3e7939e978c6 added exception CONTEXT, indicating context of another exception;
wenzelm
parents: 26081
diff changeset
   611
    in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   612
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   613
in
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   614
26602
5534b6a6b810 made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents: 26491
diff changeset
   615
fun transition int tr st =
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   616
  let
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   617
    val hooks = get_hooks ();
28103
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28095
diff changeset
   618
    fun apply_hooks st' = hooks |> List.app (fn f => (try (fn () => f tr st st') (); ()));
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   619
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   620
    val ctxt = try context_of st;
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   621
    val res =
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   622
      (case app int tr st of
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
   623
        (_, SOME Runtime.TERMINATE) => NONE
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
   624
      | (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   625
      | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
28103
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28095
diff changeset
   626
      | (st', NONE) => SOME (st', NONE));
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28095
diff changeset
   627
    val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   628
  in res end;
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   629
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   630
end;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   631
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   632
28425
25d6099179a6 export setmp_thread_position;
wenzelm
parents: 28394
diff changeset
   633
(* nested commands *)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   634
28425
25d6099179a6 export setmp_thread_position;
wenzelm
parents: 28394
diff changeset
   635
fun command tr st =
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   636
  (case transition (! interact) tr st of
28425
25d6099179a6 export setmp_thread_position;
wenzelm
parents: 28394
diff changeset
   637
    SOME (st', NONE) => st'
39285
85728a4b5620 avoid extra wrapping for interrupts;
wenzelm
parents: 39237
diff changeset
   638
  | SOME (_, SOME (exn, info)) =>
85728a4b5620 avoid extra wrapping for interrupts;
wenzelm
parents: 39237
diff changeset
   639
      if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
   640
  | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   641
29483
e959ae4a0bca added run_command (from isar_document.ML);
wenzelm
parents: 29448
diff changeset
   642
fun command_result tr st =
e959ae4a0bca added run_command (from isar_document.ML);
wenzelm
parents: 29448
diff changeset
   643
  let val st' = command tr st
e959ae4a0bca added run_command (from isar_document.ML);
wenzelm
parents: 29448
diff changeset
   644
  in (st', st') end;
e959ae4a0bca added run_command (from isar_document.ML);
wenzelm
parents: 29448
diff changeset
   645
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   646
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   647
(* excursion of units, consisting of commands with proof *)
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   648
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 33390
diff changeset
   649
structure States = Proof_Data
28974
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   650
(
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   651
  type T = state list future option;
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   652
  fun init _ = NONE;
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   653
);
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   654
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   655
fun proof_result immediate (tr, proof_trs) st =
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   656
  let val st' = command tr st in
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 35205
diff changeset
   657
    if immediate orelse
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 35205
diff changeset
   658
      null proof_trs orelse
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36355
diff changeset
   659
      Keyword.is_schematic_goal (name_of tr) orelse
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36355
diff changeset
   660
      exists (Keyword.is_qed_global o name_of) proof_trs orelse
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 35205
diff changeset
   661
      not (can proof_of st') orelse
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 35205
diff changeset
   662
      Proof.is_relevant (proof_of st')
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   663
    then
28453
06702e7acd1d excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents: 28451
diff changeset
   664
      let val (states, st'') = fold_map command_result proof_trs st'
42129
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   665
      in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end
28453
06702e7acd1d excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents: 28451
diff changeset
   666
    else
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   667
      let
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   668
        val (body_trs, end_tr) = split_last proof_trs;
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42129
diff changeset
   669
        val finish = Context.Theory o Proof_Context.theory_of;
28974
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   670
29386
d5849935560c Proof.global_future_proof;
wenzelm
parents: 29380
diff changeset
   671
        val future_proof = Proof.global_future_proof
28974
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   672
          (fn prf =>
41703
d27950860514 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents: 41674
diff changeset
   673
            Goal.fork_name "Toplevel.future_proof"
41673
1c191a39549f support named tasks, for improved tracing;
wenzelm
parents: 41536
diff changeset
   674
              (fn () =>
1c191a39549f support named tasks, for improved tracing;
wenzelm
parents: 41536
diff changeset
   675
                let val (states, result_state) =
1c191a39549f support named tasks, for improved tracing;
wenzelm
parents: 41536
diff changeset
   676
                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
1c191a39549f support named tasks, for improved tracing;
wenzelm
parents: 41536
diff changeset
   677
                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
1c191a39549f support named tasks, for improved tracing;
wenzelm
parents: 41536
diff changeset
   678
                  |> fold_map command_result body_trs
1c191a39549f support named tasks, for improved tracing;
wenzelm
parents: 41536
diff changeset
   679
                  ||> command (end_tr |> set_print false);
1c191a39549f support named tasks, for improved tracing;
wenzelm
parents: 41536
diff changeset
   680
                in (states, presentation_context_of result_state) end))
28974
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   681
          #> (fn (states, ctxt) => States.put (SOME states) ctxt);
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   682
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   683
        val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   684
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   685
        val states =
30398
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   686
          (case States.get (presentation_context_of st'') of
37852
a902f158b4fc eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
wenzelm
parents: 37711
diff changeset
   687
            NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
28974
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   688
          | SOME states => states);
42129
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   689
        val result = states
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   690
          |> Future.map (fn sts => (tr, st') :: (body_trs ~~ sts) @ [(end_tr, st'')]);
28974
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   691
d6b190efa01a excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents: 28645
diff changeset
   692
      in (result, st'') end
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   693
  end;
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   694
29068
b92443a701de removed spurious exception_trace;
wenzelm
parents: 29066
diff changeset
   695
fun excursion input =
28425
25d6099179a6 export setmp_thread_position;
wenzelm
parents: 28394
diff changeset
   696
  let
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   697
    val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
29448
34b9652b2f45 added Goal.future_enabled abstraction -- now also checks that this is already
wenzelm
parents: 29435
diff changeset
   698
    val immediate = not (Goal.future_enabled ());
29427
7ba952481e29 excursion: commit_exit internally -- checkpoints are fully persistent now;
wenzelm
parents: 29386
diff changeset
   699
    val (results, end_state) = fold_map (proof_result immediate) input toplevel;
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   700
    val thy = end_theory end_pos end_state;
42129
c17508a61f49 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
wenzelm
parents: 42012
diff changeset
   701
  in (results, thy) end;
7062
e992884b256d Toplevel.excursion_error;
wenzelm
parents: 7022
diff changeset
   702
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   703
end;