src/Pure/Isar/toplevel.ML
author wenzelm
Tue, 09 Apr 2013 20:16:52 +0200
changeset 51662 3391a493f39a
parent 51661 92e58b76dbb1
child 51735 f069c7d496ca
permissions -rw-r--r--
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
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
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
    15
  val is_skipped_proof: state -> bool
17076
c7effdf2e2e2 state: body context;
wenzelm
parents: 16815
diff changeset
    16
  val level: state -> int
30398
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
    17
  val presentation_context_of: state -> Proof.context
30801
9bdf001bea58 added Toplevel.previous_node_of;
wenzelm
parents: 30618
diff changeset
    18
  val previous_context_of: state -> Proof.context option
21506
b2a673894ce5 prefer Proof.context over Context.generic;
wenzelm
parents: 21310
diff changeset
    19
  val context_of: state -> Proof.context
22089
d9b614dc883d added generic_theory_of;
wenzelm
parents: 22056
diff changeset
    20
  val generic_theory_of: state -> generic_theory
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    21
  val theory_of: state -> theory
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    22
  val proof_of: state -> Proof.state
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
    23
  val proof_position_of: state -> int
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
    24
  val end_theory: Position.T -> state -> theory
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
    25
  val print_state_context: state -> unit
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
    26
  val print_state: bool -> state -> unit
37858
e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state;
wenzelm
parents: 37856
diff changeset
    27
  val pretty_abstract: state -> Pretty.T
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    28
  val quiet: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    29
  val debug: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    30
  val interact: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    31
  val timing: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
    32
  val profiling: int 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
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
    37
  val print_of: transition -> bool
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
    38
  val name_of: transition -> string
28105
44054657ea56 added pos_of;
wenzelm
parents: 28103
diff changeset
    39
  val pos_of: transition -> Position.T
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    40
  val name: string -> transition -> transition
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    41
  val position: Position.T -> transition -> transition
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    42
  val interactive: bool -> transition -> transition
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
    43
  val set_print: bool -> transition -> transition
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    44
  val print: transition -> transition
44187
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
    45
  val init_theory: (unit -> theory) -> transition -> transition
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
    46
  val is_init: transition -> bool
44186
806f0ec1a43d simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents: 44185
diff changeset
    47
  val modify_init: (unit -> theory) -> transition -> transition
6689
wenzelm
parents: 6664
diff changeset
    48
  val exit: transition -> transition
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    49
  val keep: (state -> unit) -> transition -> transition
7612
ba11b5db431a added keep', theory';
wenzelm
parents: 7602
diff changeset
    50
  val keep': (bool -> state -> unit) -> transition -> transition
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
    51
  val imperative: (unit -> unit) -> transition -> transition
27840
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
    52
  val ignored: Position.T -> transition
51268
fcc4b89a600d simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
wenzelm
parents: 51241
diff changeset
    53
  val is_ignored: transition -> bool
27840
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
    54
  val malformed: Position.T -> string -> transition
48772
e46cd0d26481 vacuous execution after first malformed command;
wenzelm
parents: 48633
diff changeset
    55
  val is_malformed: transition -> bool
26491
c93ff30790fe added generic_theory transaction;
wenzelm
parents: 26293
diff changeset
    56
  val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
7612
ba11b5db431a added keep', theory';
wenzelm
parents: 7602
diff changeset
    57
  val theory': (bool -> theory -> theory) -> transition -> transition
49012
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49011
diff changeset
    58
  val theory: (theory -> theory) -> transition -> transition
20985
de13e2a23c8e exit_local_theory: pass interactive flag;
wenzelm
parents: 20963
diff changeset
    59
  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
    60
  val end_local_theory: transition -> transition
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
    61
  val open_target: (generic_theory -> local_theory) -> transition -> transition
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
    62
  val close_target: transition -> transition
45488
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 44304
diff changeset
    63
  val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 44304
diff changeset
    64
    transition -> transition
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 44304
diff changeset
    65
  val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
29380
a9ee3475abf4 added local_theory';
wenzelm
parents: 29343
diff changeset
    66
    transition -> transition
45488
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 44304
diff changeset
    67
  val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
24453
86cf57ddf8f6 Added local_theory_to_proof'
berghofe
parents: 24295
diff changeset
    68
    transition -> transition
45488
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 44304
diff changeset
    69
  val local_theory_to_proof': (xstring * Position.T) option ->
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 44304
diff changeset
    70
    (bool -> local_theory -> Proof.state) -> transition -> transition
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 44304
diff changeset
    71
  val local_theory_to_proof: (xstring * Position.T) option ->
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 44304
diff changeset
    72
    (local_theory -> Proof.state) -> transition -> transition
17363
046c829c075f added three_buffersN, print3;
wenzelm
parents: 17321
diff changeset
    73
  val theory_to_proof: (theory -> Proof.state) -> transition -> transition
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
    74
  val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
    75
  val forget_proof: transition -> transition
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
    76
  val present_proof: (state -> unit) -> transition -> transition
49863
b5fb6e7f8d81 more informative errors for 'proof' and 'apply' steps;
wenzelm
parents: 49062
diff changeset
    77
  val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
17904
21c6894b5998 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents: 17513
diff changeset
    78
  val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
49863
b5fb6e7f8d81 more informative errors for 'proof' and 'apply' steps;
wenzelm
parents: 49062
diff changeset
    79
  val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
21177
e8228486aa03 removed checkpoint interface;
wenzelm
parents: 21007
diff changeset
    80
  val proof: (Proof.state -> Proof.state) -> transition -> transition
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
    81
  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
    82
  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
    83
  val skip_proof_to_theory: (int -> bool) -> transition -> transition
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
    84
  val get_id: transition -> string option
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
    85
  val put_id: string -> transition -> transition
9512
c30f6d0f81d2 added unknown_theory/proof/context;
wenzelm
parents: 9453
diff changeset
    86
  val unknown_theory: transition -> transition
c30f6d0f81d2 added unknown_theory/proof/context;
wenzelm
parents: 9453
diff changeset
    87
  val unknown_proof: transition -> transition
c30f6d0f81d2 added unknown_theory/proof/context;
wenzelm
parents: 9453
diff changeset
    88
  val unknown_context: transition -> transition
28425
25d6099179a6 export setmp_thread_position;
wenzelm
parents: 28394
diff changeset
    89
  val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27603
diff changeset
    90
  val status: transition -> Markup.T -> unit
28103
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28095
diff changeset
    91
  val add_hook: (transition -> state -> state -> unit) -> unit
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
    92
  val get_timing: transition -> Time.time option
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
    93
  val put_timing: Time.time option -> transition -> transition
26602
5534b6a6b810 made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents: 26491
diff changeset
    94
  val transition: bool -> transition -> state -> (state * (exn * string) option) option
51323
wenzelm
parents: 51322
diff changeset
    95
  val command_errors: bool -> transition -> state -> Runtime.error list * state option
51284
59a03019f3bf fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents: 51282
diff changeset
    96
  val command_exception: bool -> transition -> state -> state
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
    97
  type result
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
    98
  val join_results: result -> (transition * state) list
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
    99
  val element_result: transition Thy_Syntax.element -> state -> result * state
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   100
end;
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   101
6965
a766de752996 fixed interrupts (eliminated races);
wenzelm
parents: 6689
diff changeset
   102
structure Toplevel: TOPLEVEL =
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   103
struct
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   104
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   105
(** toplevel state **)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   106
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   107
exception UNDEF = Runtime.UNDEF;
19063
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
   108
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
   109
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   110
(* local theory wrappers *)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   111
38350
480b2de9927c renamed Theory_Target to the more appropriate Named_Target
haftmann
parents: 38236
diff changeset
   112
val loc_init = Named_Target.context_cmd;
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   113
val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   114
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   115
fun loc_begin loc (Context.Theory thy) =
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   116
      (Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy)
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   117
  | loc_begin NONE (Context.Proof lthy) =
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   118
      (Context.Proof o Local_Theory.restore, lthy)
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   119
  | loc_begin (SOME loc) (Context.Proof lthy) =
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   120
      (Context.Proof o Named_Target.reinit lthy, loc_init loc (loc_exit lthy));
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   121
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   122
21958
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   123
(* datatype node *)
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   124
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   125
datatype node =
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   126
  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
   127
    (*theory with presentation context*) |
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   128
  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
   129
    (*proof node, finish, original theory*) |
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   130
  Skipped_Proof of int * (generic_theory * generic_theory);
27564
fc6d34e49e17 replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents: 27500
diff changeset
   131
    (*proof depth, resulting theory, original theory*)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   132
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   133
val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   134
val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   135
val skipped_proof_node = fn Skipped_Proof _ => true | _ => false;
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   136
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   137
fun cases_node f _ (Theory (gthy, _)) = f gthy
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   138
  | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   139
  | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
19063
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
   140
29066
f50c24e5b9fe export context_node;
wenzelm
parents: 28999
diff changeset
   141
val context_node = cases_node Context.proof_of Proof.context_of;
f50c24e5b9fe export context_node;
wenzelm
parents: 28999
diff changeset
   142
21958
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   143
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   144
(* datatype state *)
9dfd1ca4c0a0 refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents: 21861
diff changeset
   145
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   146
datatype state = State of node option * node option;  (*current, previous*)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   147
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   148
val toplevel = State (NONE, NONE);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   149
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   150
fun is_toplevel (State (NONE, _)) = true
7732
d62523296573 added is_toplevel;
wenzelm
parents: 7612
diff changeset
   151
  | is_toplevel _ = false;
d62523296573 added is_toplevel;
wenzelm
parents: 7612
diff changeset
   152
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   153
fun level (State (NONE, _)) = 0
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   154
  | level (State (SOME (Theory _), _)) = 0
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   155
  | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   156
  | level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
17076
c7effdf2e2e2 state: body context;
wenzelm
parents: 16815
diff changeset
   157
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   158
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
   159
  | 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
   160
  | 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
   161
  | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   162
  | str_of_state (State (SOME (Skipped_Proof _), _)) = "in skipped proof mode";
5946
a4600d21b59b print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents: 5939
diff changeset
   163
a4600d21b59b print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents: 5939
diff changeset
   164
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   165
(* current node *)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   166
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   167
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
   168
  | node_of (State (SOME node, _)) = node;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   169
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   170
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
   171
fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   172
fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state);
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   173
19063
049c010c8fb7 added cases_node;
wenzelm
parents: 18955
diff changeset
   174
fun node_case f g state = cases_node f g (node_of state);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   175
30398
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   176
fun presentation_context_of state =
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   177
  (case try node_of state of
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   178
    SOME (Theory (_, SOME ctxt)) => ctxt
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   179
  | SOME node => context_node node
d7ac4b7aa590 simplified presentation_context_of;
wenzelm
parents: 30366
diff changeset
   180
  | NONE => raise UNDEF);
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   181
30801
9bdf001bea58 added Toplevel.previous_node_of;
wenzelm
parents: 30618
diff changeset
   182
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
   183
  | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
30801
9bdf001bea58 added Toplevel.previous_node_of;
wenzelm
parents: 30618
diff changeset
   184
21506
b2a673894ce5 prefer Proof.context over Context.generic;
wenzelm
parents: 21310
diff changeset
   185
val context_of = node_case Context.proof_of Proof.context_of;
22089
d9b614dc883d added generic_theory_of;
wenzelm
parents: 22056
diff changeset
   186
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
   187
val theory_of = node_case Context.theory_of Proof.theory_of;
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   188
val proof_of = node_case (fn _ => raise UNDEF) I;
17208
49bc1bdc7b6e added no_body_context;
wenzelm
parents: 17115
diff changeset
   189
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   190
fun proof_position_of state =
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   191
  (case node_of state of
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   192
    Proof (prf, _) => Proof_Node.position prf
18589
c27c9fa9e83d hide type datatype node;
wenzelm
parents: 18564
diff changeset
   193
  | _ => raise UNDEF);
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   194
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
   195
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48772
diff changeset
   196
  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48772
diff changeset
   197
  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   198
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   199
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   200
(* print state *)
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   201
38388
94d5624dd1f7 Named_Target.theory_init
haftmann
parents: 38384
diff changeset
   202
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
   203
23640
baec2e674461 toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23619
diff changeset
   204
fun print_state_context state =
24795
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   205
  (case try node_of state of
21506
b2a673894ce5 prefer Proof.context over Context.generic;
wenzelm
parents: 21310
diff changeset
   206
    NONE => []
24795
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   207
  | SOME (Theory (gthy, _)) => pretty_context gthy
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   208
  | SOME (Proof (_, (_, gthy))) => pretty_context gthy
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   209
  | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
23640
baec2e674461 toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23619
diff changeset
   210
  |> Pretty.chunks |> Pretty.writeln;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   211
23640
baec2e674461 toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23619
diff changeset
   212
fun print_state prf_only state =
23701
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   213
  (case try node_of state of
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   214
    NONE => []
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   215
  | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
1716f19e7d25 Markup.output;
wenzelm
parents: 23661
diff changeset
   216
  | SOME (Proof (prf, _)) =>
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   217
      Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   218
  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49863
diff changeset
   219
  |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   220
37858
e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state;
wenzelm
parents: 37856
diff changeset
   221
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
   222
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   223
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   224
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   225
(** toplevel transitions **)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   226
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   227
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
   228
val debug = Runtime.debug;
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   229
val interact = Unsynchronized.ref false;
42012
2c3fe3cbebae structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents: 41703
diff changeset
   230
val timing = Unsynchronized.ref false;
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   231
val profiling = Unsynchronized.ref 0;
16682
wenzelm
parents: 16658
diff changeset
   232
33604
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   233
fun program body =
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   234
 (body
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   235
  |> Runtime.controlled_execution
33604
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   236
  |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   237
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   238
fun thread interrupts body =
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   239
  Thread.fork
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 38888
diff changeset
   240
    (((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
   241
        |> Runtime.debugging
d4220df6fde2 Toplevel.thread provides Isar-style exception output;
wenzelm
parents: 33553
diff changeset
   242
        |> Runtime.toplevel_error
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39513
diff changeset
   243
          (fn exn =>
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39513
diff changeset
   244
            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
   245
      Simple_Thread.attributes interrupts);
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   246
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   247
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   248
(* node transactions -- maintaining stable checkpoints *)
7022
abf9d5e2fb6e removed BREAK, ROLLBACK;
wenzelm
parents: 6971
diff changeset
   249
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   250
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
   251
6689
wenzelm
parents: 6664
diff changeset
   252
local
wenzelm
parents: 6664
diff changeset
   253
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   254
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   255
  | reset_presentation node = node;
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   256
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   257
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
   258
  | is_draft_theory _ = false;
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   259
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents: 31431
diff changeset
   260
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
   261
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   262
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
   263
  | stale_error some = some;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   264
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   265
fun map_theory f (Theory (gthy, ctxt)) =
33671
4b0f2599ed48 modernized structure Local_Theory;
wenzelm
parents: 33604
diff changeset
   266
      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
   267
  | map_theory _ node = node;
6689
wenzelm
parents: 6664
diff changeset
   268
wenzelm
parents: 6664
diff changeset
   269
in
wenzelm
parents: 6664
diff changeset
   270
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   271
fun apply_transaction f g node =
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   272
  let
27576
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   273
    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
   274
    val cont_node = reset_presentation node;
7afff36043e6 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents: 27564
diff changeset
   275
    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
   276
    fun state_error e nd = (State (SOME nd, SOME node), e);
6689
wenzelm
parents: 6664
diff changeset
   277
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   278
    val (result, err) =
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   279
      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
   280
      |> Runtime.controlled_execution f
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   281
      |> map_theory Theory.checkpoint
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   282
      |> state_error NONE
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   283
      handle exn => state_error (SOME exn) cont_node;
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   284
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   285
    val (result', err') =
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   286
      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
   287
      else (result, err);
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   288
  in
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   289
    (case err' of
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   290
      NONE => tap g result'
26624
770265032999 transaction/init: ensure stable theory (non-draft);
wenzelm
parents: 26621
diff changeset
   291
    | SOME exn => raise FAILURE (result', exn))
20128
8f0e07d7cf92 keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents: 19996
diff changeset
   292
  end;
6689
wenzelm
parents: 6664
diff changeset
   293
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
   294
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
   295
  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
   296
    (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
   297
      | 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
   298
  #> (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
   299
6689
wenzelm
parents: 6664
diff changeset
   300
end;
wenzelm
parents: 6664
diff changeset
   301
wenzelm
parents: 6664
diff changeset
   302
wenzelm
parents: 6664
diff changeset
   303
(* primitive transitions *)
wenzelm
parents: 6664
diff changeset
   304
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   305
datatype trans =
44187
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
   306
  Init of unit -> theory |               (*init theory*)
37953
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   307
  Exit |                                 (*formal exit of theory*)
ddc3b72f9a42 simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents: 37951
diff changeset
   308
  Keep of bool -> state -> unit |        (*peek at state*)
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   309
  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
   310
6689
wenzelm
parents: 6664
diff changeset
   311
local
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   312
44187
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
   313
fun apply_tr _ (Init f) (State (NONE, _)) =
33727
e2d5d7f51aa3 init_theory: Runtime.controlled_execution for proper exception trace etc.;
wenzelm
parents: 33725
diff changeset
   314
      State (SOME (Theory (Context.Theory
44186
806f0ec1a43d simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents: 44185
diff changeset
   315
          (Theory.checkpoint (Runtime.controlled_execution f ())), 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
   316
  | 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
   317
      exit_transaction state
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   318
  | 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
   319
      Runtime.controlled_execution (fn x => tap (f int) x) state
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   320
  | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   321
      apply_transaction (fn x => f int x) g state
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   322
  | apply_tr _ _ _ = raise UNDEF;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   323
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   324
fun apply_union _ [] state = raise FAILURE (state, UNDEF)
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   325
  | apply_union int (tr :: trs) state =
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   326
      apply_union int trs state
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   327
        handle Runtime.UNDEF => apply_tr int tr state
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   328
          | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state
6689
wenzelm
parents: 6664
diff changeset
   329
          | exn as FAILURE _ => raise exn
wenzelm
parents: 6664
diff changeset
   330
          | exn => raise FAILURE (state, exn);
wenzelm
parents: 6664
diff changeset
   331
wenzelm
parents: 6664
diff changeset
   332
in
wenzelm
parents: 6664
diff changeset
   333
32792
a08a2b962a09 eliminated dead code;
wenzelm
parents: 32738
diff changeset
   334
fun apply_trans int trs state = (apply_union int trs state, NONE)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15519
diff changeset
   335
  handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
6689
wenzelm
parents: 6664
diff changeset
   336
wenzelm
parents: 6664
diff changeset
   337
end;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   338
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   339
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   340
(* datatype transition *)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   341
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   342
datatype transition = Transition of
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   343
 {name: string,              (*command name*)
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   344
  pos: Position.T,           (*source position*)
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   345
  int_only: bool,            (*interactive-only*)
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   346
  print: bool,               (*print result state*)
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   347
  timing: Time.time option,  (*prescient timing information*)
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   348
  trans: trans list};        (*primitive transitions (union)*)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   349
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   350
fun make_transition (name, pos, int_only, print, timing, trans) =
51217
65ab2c4f4c32 support for prescient timing information within command transactions;
wenzelm
parents: 51216
diff changeset
   351
  Transition {name = name, pos = pos, int_only = int_only, print = print,
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   352
    timing = timing, trans = trans};
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   353
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   354
fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) =
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   355
  make_transition (f (name, pos, int_only, print, timing, trans));
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   356
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   357
val empty = make_transition ("", Position.none, false, false, NONE, []);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   358
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   359
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   360
(* diagnostics *)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   361
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
   362
fun print_of (Transition {print, ...}) = print;
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   363
fun name_of (Transition {name, ...}) = name;
28105
44054657ea56 added pos_of;
wenzelm
parents: 28103
diff changeset
   364
fun pos_of (Transition {pos, ...}) = pos;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   365
48993
44428ea53dc1 tuned signature;
wenzelm
parents: 48992
diff changeset
   366
fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr);
38875
c7a66b584147 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents: 38721
diff changeset
   367
fun at_command tr = command_msg "At " tr;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   368
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   369
fun type_error tr state =
18685
725660906cb3 sane ERROR vs. TOPLEVEL_ERROR handling;
wenzelm
parents: 18664
diff changeset
   370
  ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   371
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   372
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   373
(* modify transitions *)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   374
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   375
fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) =>
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   376
  (name, pos, int_only, print, timing, trans));
9010
ce78dc5e1a73 Toplevel.no_timing;
wenzelm
parents: 8999
diff changeset
   377
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   378
fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) =>
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   379
  (name, pos, int_only, print, timing, trans));
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   380
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   381
fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) =>
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   382
  (name, pos, int_only, print, timing, trans));
14923
8a32071c3c13 added name_of, source_of, source;
wenzelm
parents: 14825
diff changeset
   383
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   384
fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) =>
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   385
  (name, pos, int_only, print, timing, tr :: trans));
16607
81e687c63e29 added print': print depending on print_mode;
wenzelm
parents: 16490
diff changeset
   386
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   387
val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) =>
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   388
  (name, pos, int_only, print, timing, []));
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   389
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   390
fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) =>
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   391
  (name, pos, int_only, print, timing, trans));
28453
06702e7acd1d excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents: 28451
diff changeset
   392
06702e7acd1d excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents: 28451
diff changeset
   393
val print = set_print true;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   394
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   395
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   396
(* basic transitions *)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   397
44187
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
   398
fun init_theory f = add_trans (Init f);
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
   399
44187
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
   400
fun is_init (Transition {trans = [Init _], ...}) = true
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
   401
  | is_init _ = false;
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
   402
88d770052bac simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents: 44186
diff changeset
   403
fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else 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
   404
6689
wenzelm
parents: 6664
diff changeset
   405
val exit = add_trans Exit;
7612
ba11b5db431a added keep', theory';
wenzelm
parents: 7602
diff changeset
   406
val keep' = add_trans o Keep;
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   407
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   408
fun present_transaction f g = add_trans (Transaction (f, g));
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   409
fun transaction f = present_transaction f (K ());
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   410
7612
ba11b5db431a added keep', theory';
wenzelm
parents: 7602
diff changeset
   411
fun keep f = add_trans (Keep (fn _ => f));
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   412
fun imperative f = keep (fn _ => f ());
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   413
27840
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
   414
fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
51268
fcc4b89a600d simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
wenzelm
parents: 51241
diff changeset
   415
fun is_ignored tr = name_of tr = "<ignored>";
48772
e46cd0d26481 vacuous execution after first malformed command;
wenzelm
parents: 48633
diff changeset
   416
e46cd0d26481 vacuous execution after first malformed command;
wenzelm
parents: 48633
diff changeset
   417
val malformed_name = "<malformed>";
27840
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
   418
fun malformed pos msg =
48772
e46cd0d26481 vacuous execution after first malformed command;
wenzelm
parents: 48633
diff changeset
   419
  empty |> name malformed_name |> position pos |> imperative (fn () => error msg);
e46cd0d26481 vacuous execution after first malformed command;
wenzelm
parents: 48633
diff changeset
   420
fun is_malformed tr = name_of tr = malformed_name;
27840
e9483ef084cc added ignored, malformed transitions;
wenzelm
parents: 27606
diff changeset
   421
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   422
val unknown_theory = imperative (fn () => warning "Unknown theory context");
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   423
val unknown_proof = imperative (fn () => warning "Unknown proof context");
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   424
val unknown_context = imperative (fn () => warning "Unknown context");
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   425
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   426
49012
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49011
diff changeset
   427
(* theory transitions *)
44304
7ee000ce5390 maintain recent future proofs at transaction boundaries;
wenzelm
parents: 44270
diff changeset
   428
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   429
fun generic_theory f = transaction (fn _ =>
26491
c93ff30790fe added generic_theory transaction;
wenzelm
parents: 26293
diff changeset
   430
  (fn Theory (gthy, _) => Theory (f gthy, NONE)
c93ff30790fe added generic_theory transaction;
wenzelm
parents: 26293
diff changeset
   431
    | _ => raise UNDEF));
c93ff30790fe added generic_theory transaction;
wenzelm
parents: 26293
diff changeset
   432
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   433
fun theory' f = transaction (fn int =>
33725
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   434
  (fn Theory (Context.Theory thy, _) =>
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   435
      let val thy' = thy
49012
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49011
diff changeset
   436
        |> Sign.new_group
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49011
diff changeset
   437
        |> Theory.checkpoint
33725
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   438
        |> f int
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   439
        |> Sign.reset_group;
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   440
      in Theory (Context.Theory thy', NONE) end
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   441
    | _ => raise UNDEF));
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   442
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   443
fun theory f = theory' (K f);
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   444
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   445
fun begin_local_theory begin f = transaction (fn _ =>
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   446
  (fn Theory (Context.Theory thy, _) =>
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   447
        let
20985
de13e2a23c8e exit_local_theory: pass interactive flag;
wenzelm
parents: 20963
diff changeset
   448
          val lthy = f thy;
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   449
          val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   450
        in Theory (gthy, SOME lthy) end
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   451
    | _ => raise UNDEF));
17076
c7effdf2e2e2 state: body context;
wenzelm
parents: 16815
diff changeset
   452
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   453
val end_local_theory = transaction (fn _ =>
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   454
  (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
   455
    | _ => raise UNDEF));
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   456
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   457
fun open_target f = transaction (fn _ =>
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   458
  (fn Theory (gthy, _) =>
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   459
        let val lthy = f gthy
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   460
        in Theory (Context.Proof lthy, SOME lthy) end
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   461
    | _ => raise UNDEF));
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   462
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   463
val close_target = transaction (fn _ =>
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   464
  (fn Theory (Context.Proof lthy, _) =>
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   465
        (case try Local_Theory.close_target lthy of
50739
5165d7e6d3b9 more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents: 50201
diff changeset
   466
          SOME ctxt' =>
5165d7e6d3b9 more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents: 50201
diff changeset
   467
            let
5165d7e6d3b9 more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents: 50201
diff changeset
   468
              val gthy' =
5165d7e6d3b9 more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents: 50201
diff changeset
   469
                if can Local_Theory.assert ctxt'
5165d7e6d3b9 more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents: 50201
diff changeset
   470
                then Context.Proof ctxt'
5165d7e6d3b9 more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents: 50201
diff changeset
   471
                else Context.Theory (Proof_Context.theory_of ctxt');
5165d7e6d3b9 more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents: 50201
diff changeset
   472
            in Theory (gthy', SOME lthy) end
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   473
        | NONE => raise UNDEF)
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   474
    | _ => raise UNDEF));
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   475
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 46959
diff changeset
   476
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   477
local
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   478
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   479
fun local_theory_presentation loc f = present_transaction (fn int =>
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   480
  (fn Theory (gthy, _) =>
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   481
        let
49062
7e31dfd99ce7 discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents: 49042
diff changeset
   482
          val (finish, lthy) = loc_begin loc gthy;
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   483
          val lthy' = lthy
49012
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49011
diff changeset
   484
            |> Local_Theory.new_group
33725
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   485
            |> f int
a8481da77270 implicit name space grouping for theory/local_theory transactions;
wenzelm
parents: 33671
diff changeset
   486
            |> Local_Theory.reset_group;
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   487
        in Theory (finish lthy', SOME lthy') end
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   488
    | _ => raise UNDEF));
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   489
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   490
in
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   491
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   492
fun local_theory' loc f = local_theory_presentation loc f (K ());
29380
a9ee3475abf4 added local_theory';
wenzelm
parents: 29343
diff changeset
   493
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
   494
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
   495
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   496
end;
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   497
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   498
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   499
(* proof transitions *)
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   500
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   501
fun end_proof f = transaction (fn int =>
24795
6f5cb7885fd7 print_state_context: local theory context, not proof context;
wenzelm
parents: 24780
diff changeset
   502
  (fn Proof (prf, (finish, _)) =>
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33223
diff changeset
   503
        let val state = Proof_Node.current prf in
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   504
          if can (Proof.assert_bottom true) state then
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   505
            let
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   506
              val ctxt' = f int state;
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   507
              val gthy' = finish ctxt';
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   508
            in Theory (gthy', SOME ctxt') end
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   509
          else raise UNDEF
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   510
        end
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   511
    | Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE)
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   512
    | _ => raise UNDEF));
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   513
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   514
local
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   515
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   516
fun begin_proof init = transaction (fn int =>
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   517
  (fn Theory (gthy, _) =>
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   518
    let
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   519
      val (finish, prf) = init int gthy;
51553
63327f679cff more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents: 51423
diff changeset
   520
      val skip = ! Goal.skip_proofs;
40960
9e54eb514a46 formal notepad without any result;
wenzelm
parents: 40132
diff changeset
   521
      val (is_goal, no_skip) =
9e54eb514a46 formal notepad without any result;
wenzelm
parents: 40132
diff changeset
   522
        (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   523
      val _ =
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   524
        if is_goal andalso skip andalso no_skip then
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   525
          warning "Cannot skip proof of schematic goal statement"
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   526
        else ();
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   527
    in
40960
9e54eb514a46 formal notepad without any result;
wenzelm
parents: 40132
diff changeset
   528
      if skip andalso not no_skip then
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   529
        Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy))
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   530
      else Proof (Proof_Node.init prf, (finish, gthy))
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   531
    end
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   532
  | _ => raise UNDEF));
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   533
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   534
in
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   535
24780
47bb1e380d83 local_theory transactions: more careful treatment of context position;
wenzelm
parents: 24634
diff changeset
   536
fun local_theory_to_proof' loc f = begin_proof
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   537
  (fn int => fn gthy =>
49062
7e31dfd99ce7 discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents: 49042
diff changeset
   538
    let val (finish, lthy) = loc_begin loc gthy
49012
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49011
diff changeset
   539
    in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
24780
47bb1e380d83 local_theory transactions: more careful treatment of context position;
wenzelm
parents: 24634
diff changeset
   540
24453
86cf57ddf8f6 Added local_theory_to_proof'
berghofe
parents: 24295
diff changeset
   541
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
   542
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   543
fun theory_to_proof f = begin_proof
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47069
diff changeset
   544
  (fn _ => fn gthy =>
51560
5b4ae2467830 extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
wenzelm
parents: 51555
diff changeset
   545
    (Context.Theory o Theory.checkpoint o Sign.reset_group o Proof_Context.theory_of,
49062
7e31dfd99ce7 discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents: 49042
diff changeset
   546
      (case gthy of
49012
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49011
diff changeset
   547
        Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 49011
diff changeset
   548
      | _ => raise UNDEF)));
21294
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   549
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   550
end;
5cd48242ef17 simplified local theory wrappers;
wenzelm
parents: 21277
diff changeset
   551
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   552
val forget_proof = transaction (fn _ =>
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   553
  (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   554
    | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   555
    | _ => raise UNDEF));
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   556
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   557
val present_proof = present_transaction (fn _ =>
49062
7e31dfd99ce7 discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents: 49042
diff changeset
   558
  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   559
    | skip as Skipped_Proof _ => skip
30366
e3d788b9dffb simplified presentation: built into transaction, pass state directly;
wenzelm
parents: 29516
diff changeset
   560
    | _ => raise UNDEF));
21177
e8228486aa03 removed checkpoint interface;
wenzelm
parents: 21007
diff changeset
   561
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   562
fun proofs' f = transaction (fn int =>
49062
7e31dfd99ce7 discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents: 49042
diff changeset
   563
  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   564
    | skip as Skipped_Proof _ => skip
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   565
    | _ => raise UNDEF));
15668
53c049a365cf improved exn_message;
wenzelm
parents: 15633
diff changeset
   566
49863
b5fb6e7f8d81 more informative errors for 'proof' and 'apply' steps;
wenzelm
parents: 49062
diff changeset
   567
fun proof' f = proofs' ((Seq.single o Seq.Result) oo f);
17904
21c6894b5998 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents: 17513
diff changeset
   568
val proofs = proofs' o K;
6689
wenzelm
parents: 6664
diff changeset
   569
val proof = proof' o K;
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   570
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   571
fun actual_proof f = transaction (fn _ =>
21007
1bbb31aaf98d renamed enter_forward_proof to enter_proof_body;
wenzelm
parents: 20985
diff changeset
   572
  (fn Proof (prf, x) => Proof (f prf, x)
20963
a7fd8f05a2be added type global_theory -- theory or local_theory;
wenzelm
parents: 20928
diff changeset
   573
    | _ => raise UNDEF));
16815
13d20ed9086c added print_state_hook;
wenzelm
parents: 16729
diff changeset
   574
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   575
fun skip_proof f = transaction (fn _ =>
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   576
  (fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
18563
wenzelm
parents: 17904
diff changeset
   577
    | _ => raise UNDEF));
wenzelm
parents: 17904
diff changeset
   578
27601
6683cdb94af8 simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents: 27583
diff changeset
   579
fun skip_proof_to_theory pred = transaction (fn _ =>
51555
6aa64925db77 explicit Toplevel.is_skipped_proof;
wenzelm
parents: 51553
diff changeset
   580
  (fn Skipped_Proof (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
   581
    | _ => raise UNDEF));
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   582
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   583
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   584
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   585
(** toplevel transactions **)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   586
27427
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   587
(* identification *)
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   588
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   589
fun get_id (Transition {pos, ...}) = Position.get_id pos;
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   590
fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   591
f6751d265cf6 added name_of;
wenzelm
parents: 26982
diff changeset
   592
25960
1f9956e0bd89 removed unused properties;
wenzelm
parents: 25847
diff changeset
   593
(* thread position *)
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   594
25960
1f9956e0bd89 removed unused properties;
wenzelm
parents: 25847
diff changeset
   595
fun setmp_thread_position (Transition {pos, ...}) f x =
25819
e6feb08b7f4b replaced thread_properties by simplified version in position.ML;
wenzelm
parents: 25809
diff changeset
   596
  Position.setmp_thread_data pos f x;
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   597
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27603
diff changeset
   598
fun status tr m =
43665
573d1272f36d tuned signature;
wenzelm
parents: 42360
diff changeset
   599
  setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
27606
82399f3a8ca8 support for command status;
wenzelm
parents: 27603
diff changeset
   600
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   601
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   602
(* post-transition hooks *)
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   603
37905
wenzelm
parents: 37865
diff changeset
   604
local
wenzelm
parents: 37865
diff changeset
   605
  val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
wenzelm
parents: 37865
diff changeset
   606
in
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   607
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32062
diff changeset
   608
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
33223
d27956b4d3b4 non-critical atomic accesses;
wenzelm
parents: 32792
diff changeset
   609
fun get_hooks () = ! hooks;
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   610
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   611
end;
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   612
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   613
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   614
(* apply transitions *)
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   615
51217
65ab2c4f4c32 support for prescient timing information within command transactions;
wenzelm
parents: 51216
diff changeset
   616
fun get_timing (Transition {timing, ...}) = timing;
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   617
fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   618
  (name, pos, int_only, print, timing, trans));
51217
65ab2c4f4c32 support for prescient timing information within command transactions;
wenzelm
parents: 51216
diff changeset
   619
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   620
local
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   621
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   622
fun app int (tr as Transition {trans, print, ...}) =
25819
e6feb08b7f4b replaced thread_properties by simplified version in position.ML;
wenzelm
parents: 25809
diff changeset
   623
  setmp_thread_position tr (fn state =>
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   624
    let
51595
8e9746e584c9 more centralized command timing;
wenzelm
parents: 51560
diff changeset
   625
      val timing_start = Timing.start ();
25799
7a204e0467f8 maintain thread transition properties;
wenzelm
parents: 25796
diff changeset
   626
51595
8e9746e584c9 more centralized command timing;
wenzelm
parents: 51560
diff changeset
   627
      val (result, opt_err) =
51658
21c10672633b discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents: 51605
diff changeset
   628
         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
26621
78b3ad7af5d5 eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents: 26602
diff changeset
   629
      val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
51216
e6e7685fc8f8 emit command_timing properties into build log;
wenzelm
parents: 50917
diff changeset
   630
51595
8e9746e584c9 more centralized command timing;
wenzelm
parents: 51560
diff changeset
   631
      val timing_result = Timing.result timing_start;
51662
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51661
diff changeset
   632
      val timing_props =
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51661
diff changeset
   633
        Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
3391a493f39a just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents: 51661
diff changeset
   634
      val _ = Timing.protocol_message timing_props timing_result;
51595
8e9746e584c9 more centralized command timing;
wenzelm
parents: 51560
diff changeset
   635
    in
8e9746e584c9 more centralized command timing;
wenzelm
parents: 51560
diff changeset
   636
      (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
8e9746e584c9 more centralized command timing;
wenzelm
parents: 51560
diff changeset
   637
    end);
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   638
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   639
in
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   640
26602
5534b6a6b810 made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents: 26491
diff changeset
   641
fun transition int tr st =
28095
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   642
  let
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   643
    val hooks = get_hooks ();
28103
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28095
diff changeset
   644
    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
   645
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   646
    val ctxt = try context_of st;
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   647
    val res =
7eaf0813bdc3 added add_hook interface for post-transition hooks;
wenzelm
parents: 27859
diff changeset
   648
      (case app int tr st of
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
   649
        (_, SOME Runtime.TERMINATE) => NONE
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38876
diff changeset
   650
      | (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
   651
      | (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
   652
      | (st', NONE) => SOME (st', NONE));
b79e61861f0f simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents: 28095
diff changeset
   653
    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
   654
  in res end;
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   655
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   656
end;
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   657
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   658
51284
59a03019f3bf fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents: 51282
diff changeset
   659
(* managed commands *)
5828
1feeadaad6a9 The Isabelle/Isar toplevel.
wenzelm
parents:
diff changeset
   660
51323
wenzelm
parents: 51322
diff changeset
   661
fun command_errors int tr st =
wenzelm
parents: 51322
diff changeset
   662
  (case transition int tr st of
wenzelm
parents: 51322
diff changeset
   663
    SOME (st', NONE) => ([], SOME st')
wenzelm
parents: 51322
diff changeset
   664
  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
wenzelm
parents: 51322
diff changeset
   665
  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
wenzelm
parents: 51322
diff changeset
   666
51284
59a03019f3bf fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents: 51282
diff changeset
   667
fun command_exception int tr st =
59a03019f3bf fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents: 51282
diff changeset
   668
  (case transition int tr st of
28425
25d6099179a6 export setmp_thread_position;
wenzelm
parents: 28394
diff changeset
   669
    SOME (st', NONE) => st'
39285
85728a4b5620 avoid extra wrapping for interrupts;
wenzelm
parents: 39237
diff changeset
   670
  | SOME (_, SOME (exn, info)) =>
85728a4b5620 avoid extra wrapping for interrupts;
wenzelm
parents: 39237
diff changeset
   671
      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
   672
  | 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
   673
51323
wenzelm
parents: 51322
diff changeset
   674
fun command tr = command_exception (! interact) tr;
51284
59a03019f3bf fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents: 51282
diff changeset
   675
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   676
46959
cdc791910460 defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm
parents: 45666
diff changeset
   677
(* scheduled proof result *)
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   678
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   679
datatype result =
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   680
  Result of transition * state |
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   681
  Result_List of result list |
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   682
  Result_Future of result future;
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   683
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   684
fun join_results (Result x) = [x]
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   685
  | join_results (Result_List xs) = maps join_results xs
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   686
  | join_results (Result_Future x) = join_results (Future.join x);
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   687
51323
wenzelm
parents: 51322
diff changeset
   688
local
wenzelm
parents: 51322
diff changeset
   689
47417
9679bab23f93 misc tuning and simplification;
wenzelm
parents: 47416
diff changeset
   690
structure Result = 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
   691
(
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   692
  type T = result;
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   693
  val empty: T = Result_List [];
47417
9679bab23f93 misc tuning and simplification;
wenzelm
parents: 47416
diff changeset
   694
  fun init _ = empty;
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
   695
);
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
   696
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   697
val get_result = Result.get o Proof.context_of;
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   698
val put_result = Proof.map_context o Result.put;
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   699
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   700
fun timing_estimate include_head elem =
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   701
  let
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   702
    val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   703
    val timings = map get_timing trs;
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   704
  in
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   705
    if forall is_some timings then
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   706
      SOME (fold (curry Time.+ o the) timings Time.zeroTime)
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   707
    else NONE
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   708
  end;
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   709
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   710
fun priority NONE = ~1
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   711
  | priority (SOME estimate) =
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   712
      Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   713
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   714
fun proof_future_enabled estimate st =
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   715
  (case try proof_of st of
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   716
    NONE => false
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   717
  | SOME state =>
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   718
      not (Proof.is_relevant state) andalso
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   719
       (if can (Proof.assert_bottom true) state
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   720
        then Goal.future_enabled ()
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   721
        else
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   722
          (case estimate of
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   723
            NONE => Goal.future_enabled_nested 2
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   724
          | SOME t => Goal.future_enabled_timing t)));
51278
wenzelm
parents: 51274
diff changeset
   725
51323
wenzelm
parents: 51322
diff changeset
   726
fun atom_result tr st =
wenzelm
parents: 51322
diff changeset
   727
  let
wenzelm
parents: 51322
diff changeset
   728
    val st' =
wenzelm
parents: 51322
diff changeset
   729
      if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
51605
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   730
        (Goal.fork_params
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   731
          {name = "Toplevel.diag", pos = pos_of tr,
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   732
            pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   733
          (fn () => command tr st); st)
51323
wenzelm
parents: 51322
diff changeset
   734
      else command tr st;
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   735
  in (Result (tr, st'), st') end;
51323
wenzelm
parents: 51322
diff changeset
   736
wenzelm
parents: 51322
diff changeset
   737
in
wenzelm
parents: 51322
diff changeset
   738
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   739
fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   740
  | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
48633
7cd32f9d4293 recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
wenzelm
parents: 47881
diff changeset
   741
      let
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   742
        val (head_result, st') = atom_result head_tr st;
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   743
        val (body_elems, end_tr) = element_rest;
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   744
        val estimate = timing_estimate false elem;
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   745
      in
51423
e5f9a6d9ca82 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents: 51332
diff changeset
   746
        if not (proof_future_enabled estimate st')
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   747
        then
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   748
          let
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   749
            val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   750
            val (proof_results, st'') = fold_map atom_result proof_trs st';
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   751
          in (Result_List (head_result :: proof_results), st'') end
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   752
        else
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   753
          let
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   754
            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
   755
51605
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   756
            val future_proof =
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   757
              Proof.future_proof (fn state =>
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   758
                Goal.fork_params
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   759
                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   760
                  (fn () =>
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   761
                    let
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   762
                      val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   763
                      val prf' = Proof_Node.apply (K state) prf;
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   764
                      val (result, result_state) =
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   765
                        State (SOME (Proof (prf', (finish, orig_gthy))), prev)
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   766
                        |> fold_map element_result body_elems ||> command end_tr;
eca8acb42e4a more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents: 51595
diff changeset
   767
                    in (Result_List result, presentation_context_of result_state) end))
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   768
              #> (fn (res, state') => state' |> put_result (Result_Future res));
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   769
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   770
            val forked_proof =
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   771
              proof (future_proof #>
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   772
                (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   773
              end_proof (fn _ => future_proof #>
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   774
                (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
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
   775
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   776
            val st'' = st'
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   777
              |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   778
            val end_result = Result (end_tr, st'');
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   779
            val result =
51332
8707df0b0255 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents: 51324
diff changeset
   780
              Result_List [head_result, Result.get (presentation_context_of st''), end_result];
51324
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   781
          in (result, st'') end
c17f5de0a915 uniform treatment of global/local proofs;
wenzelm
parents: 51323
diff changeset
   782
      end;
28433
b3dab95f098f begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents: 28425
diff changeset
   783
6664
f679ddd1ddd8 cleaned comments;
wenzelm
parents: 6244
diff changeset
   784
end;
51323
wenzelm
parents: 51322
diff changeset
   785
wenzelm
parents: 51322
diff changeset
   786
end;