src/Pure/Isar/isar_cmd.ML
author wenzelm
Thu, 16 Apr 2015 16:19:39 +0200
changeset 60098 3c66b0a9d7b0
parent 60097 d20ca79d50e4
child 60378 26dcc7f19b02
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/isar_cmd.ML
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
     3
30805
wenzelm
parents: 30801
diff changeset
     4
Miscellaneous Isar commands.
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
     5
*)
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
     6
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
     7
signature ISAR_CMD =
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
     8
sig
59930
bdbc4b761c31 tuned signature;
wenzelm
parents: 59917
diff changeset
     9
  val setup: Input.source -> theory -> theory
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    10
  val local_setup: Input.source -> Proof.context -> Proof.context
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    11
  val parse_ast_translation: Input.source -> theory -> theory
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    12
  val parse_translation: Input.source -> theory -> theory
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    13
  val print_translation: Input.source -> theory -> theory
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    14
  val typed_print_translation: Input.source -> theory -> theory
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    15
  val print_ast_translation: Input.source -> theory -> theory
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
    16
  val translations: (xstring * string) Syntax.trrule list -> theory -> theory
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
    17
  val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    18
  val oracle: bstring * Position.range -> Input.source -> theory -> theory
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57934
diff changeset
    19
  val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    20
  val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    21
  val simproc_setup: string * Position.T -> string list -> Input.source ->
42464
ae16b8abf1a8 proper binding/report of defined simprocs;
wenzelm
parents: 42425
diff changeset
    22
    string list -> local_theory -> local_theory
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    23
  val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    24
  val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    25
  val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28083
diff changeset
    26
  val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
49889
00ea087e83d8 more method position information, notably finished_pos after end of previous text;
wenzelm
parents: 49866
diff changeset
    27
  val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
00ea087e83d8 more method position information, notably finished_pos after end of previous text;
wenzelm
parents: 49866
diff changeset
    28
  val terminal_proof: Method.text_range * Method.text_range option ->
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
    29
    Toplevel.transition -> Toplevel.transition
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
    30
  val default_proof: Toplevel.transition -> Toplevel.transition
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
    31
  val immediate_proof: Toplevel.transition -> Toplevel.transition
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
    32
  val done_proof: Toplevel.transition -> Toplevel.transition
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
    33
  val skip_proof: Toplevel.transition -> Toplevel.transition
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    34
  val ml_diag: bool -> Input.source -> Toplevel.transition -> Toplevel.transition
48776
37cd53e69840 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents: 47815
diff changeset
    35
  val diag_state: Proof.context -> Toplevel.state
37cd53e69840 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents: 47815
diff changeset
    36
  val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
57605
8e0a7eaffe47 tuned messages;
wenzelm
parents: 56868
diff changeset
    37
  val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57934
diff changeset
    38
  val print_stmts: string list * (Facts.ref * Token.src list) list
19268
5a575522fd26 added print_stmts;
wenzelm
parents: 19057
diff changeset
    39
    -> Toplevel.transition -> Toplevel.transition
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57934
diff changeset
    40
  val print_thms: string list * (Facts.ref * Token.src list) list
10581
74e542a299f0 dignostic commands: comment;
wenzelm
parents: 9731
diff changeset
    41
    -> Toplevel.transition -> Toplevel.transition
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 57934
diff changeset
    42
  val print_prfs: bool -> string list * (Facts.ref * Token.src list) list option
11524
197f2e14a714 Added functions for printing primitive proof terms.
berghofe
parents: 11017
diff changeset
    43
    -> Toplevel.transition -> Toplevel.transition
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12758
diff changeset
    44
  val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12758
diff changeset
    45
  val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
48792
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
    46
  val print_type: (string list * (string * string option)) ->
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
    47
    Toplevel.transition -> Toplevel.transition
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
    48
end;
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
    49
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    50
structure Isar_Cmd: ISAR_CMD =
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
    51
struct
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
    52
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
    53
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    54
(** theory declarations **)
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    55
30461
00323c45ea83 added 'local_setup' command;
wenzelm
parents: 30367
diff changeset
    56
(* generic setup *)
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    57
59930
bdbc4b761c31 tuned signature;
wenzelm
parents: 59917
diff changeset
    58
fun setup source =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
    59
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    60
  |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
    61
    "Context.map_theory setup"
26435
bdce320cd426 eliminated delayed theory setup
wenzelm
parents: 26425
diff changeset
    62
  |> Context.theory_map;
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    63
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
    64
fun local_setup source =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
    65
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    66
  |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
    67
    "Context.map_proof local_setup"
30461
00323c45ea83 added 'local_setup' command;
wenzelm
parents: 30367
diff changeset
    68
  |> Context.proof_map;
00323c45ea83 added 'local_setup' command;
wenzelm
parents: 30367
diff changeset
    69
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    70
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    71
(* translation functions *)
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    72
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
    73
fun parse_ast_translation source =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
    74
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    75
  |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
    76
    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51717
diff changeset
    77
    "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    78
  |> Context.theory_map;
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    79
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
    80
fun parse_translation source =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
    81
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    82
  |> ML_Context.expression (Input.range_of source) "parse_translation"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
    83
    "(string * (Proof.context -> term list -> term)) list"
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51717
diff changeset
    84
    "Context.map_theory (Sign.parse_translation parse_translation)"
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51717
diff changeset
    85
  |> Context.theory_map;
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51717
diff changeset
    86
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
    87
fun print_translation source =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
    88
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    89
  |> ML_Context.expression (Input.range_of source) "print_translation"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
    90
    "(string * (Proof.context -> term list -> term)) list"
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51717
diff changeset
    91
    "Context.map_theory (Sign.print_translation print_translation)"
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    92
  |> Context.theory_map;
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    93
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
    94
fun typed_print_translation source =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
    95
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    96
  |> ML_Context.expression (Input.range_of source) "typed_print_translation"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
    97
    "(string * (Proof.context -> typ -> term list -> term)) list"
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51717
diff changeset
    98
    "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
    99
  |> Context.theory_map;
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
   100
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
   101
fun print_ast_translation source =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
   102
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
   103
  |> ML_Context.expression (Input.range_of source) "print_ast_translation"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
   104
    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51717
diff changeset
   105
    "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
   106
  |> Context.theory_map;
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
   107
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
   108
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   109
(* translation rules *)
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   110
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   111
fun read_trrules thy raw_rules =
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   112
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   113
    val ctxt = Proof_Context.init_global thy;
56006
6a4dcaf53664 more formal read_root;
wenzelm
parents: 56005
diff changeset
   114
    val read_root =
6a4dcaf53664 more formal read_root;
wenzelm
parents: 56005
diff changeset
   115
      #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   116
  in
56006
6a4dcaf53664 more formal read_root;
wenzelm
parents: 56005
diff changeset
   117
    raw_rules
6a4dcaf53664 more formal read_root;
wenzelm
parents: 56005
diff changeset
   118
    |> map (Syntax.map_trrule (fn (r, s) => Syntax_Phases.parse_ast_pattern ctxt (read_root r, s)))
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   119
  end;
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   120
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   121
fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   122
fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy;
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   123
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41435
diff changeset
   124
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
   125
(* oracles *)
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
   126
59029
c907cbe36713 more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58991
diff changeset
   127
fun oracle (name, range) source =
27871
4ef76f8788ad oracle, header/local_theory/proof_markup: pass SymbolPos.text;
wenzelm
parents: 27853
diff changeset
   128
  let
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
   129
    val body_range = Input.range_of source;
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
   130
    val body = ML_Lex.read_source false source;
59029
c907cbe36713 more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58991
diff changeset
   131
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   132
    val ants =
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59064
diff changeset
   133
      ML_Lex.read
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   134
       ("local\n\
59029
c907cbe36713 more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58991
diff changeset
   135
        \  val binding = " ^ ML_Syntax.make_binding (name, #1 range) ^ ";\n\
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59064
diff changeset
   136
        \  val") @ ML_Lex.read_set_range body_range "oracle" @ ML_Lex.read "=" @ body @
dd8ec9138112 tuned signature;
wenzelm
parents: 59064
diff changeset
   137
        ML_Lex.read (";\nin\n\
dd8ec9138112 tuned signature;
wenzelm
parents: 59064
diff changeset
   138
        \  val") @ ML_Lex.read_set_range range name @ ML_Lex.read "=\
59029
c907cbe36713 more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58991
diff changeset
   139
        \ snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
c907cbe36713 more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58991
diff changeset
   140
        \end;\n";
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   141
  in
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   142
    Context.theory_map
59029
c907cbe36713 more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58991
diff changeset
   143
      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 body_range) ants))
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   144
  end;
22116
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
   145
6917be2e647d added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents: 22087
diff changeset
   146
50737
f310d1735d93 tuned -- less indirection;
wenzelm
parents: 49889
diff changeset
   147
(* old-style defs *)
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   148
35852
4e3fe0b8687b minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
wenzelm
parents: 35141
diff changeset
   149
fun add_defs ((unchecked, overloaded), args) thy =
57683
cc0aa6528890 old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
wenzelm
parents: 57605
diff changeset
   150
 (legacy_feature "Old 'defs' command -- use 'definition' (with 'overloading') instead";
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
   151
  thy |>
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39507
diff changeset
   152
    (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
47815
43f677b3ae91 clarified signature;
wenzelm
parents: 46922
diff changeset
   153
      overloaded
43f677b3ae91 clarified signature;
wenzelm
parents: 46922
diff changeset
   154
      (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
57683
cc0aa6528890 old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
wenzelm
parents: 57605
diff changeset
   155
  |> snd);
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   156
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   157
22087
a13299166175 added 'declaration' command;
wenzelm
parents: 21955
diff changeset
   158
(* declarations *)
a13299166175 added 'declaration' command;
wenzelm
parents: 21955
diff changeset
   159
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
   160
fun declaration {syntax, pervasive} source =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
   161
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
   162
  |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
45291
57cd50f98fdc uniform Local_Theory.declaration with explicit params;
wenzelm
parents: 44338
diff changeset
   163
    ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
57cd50f98fdc uniform Local_Theory.declaration with explicit params;
wenzelm
parents: 44338
diff changeset
   164
      \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
26385
ae7564661e76 ML runtime compilation: pass position, tuned signature;
wenzelm
parents: 26336
diff changeset
   165
  |> Context.proof_map;
22087
a13299166175 added 'declaration' command;
wenzelm
parents: 21955
diff changeset
   166
a13299166175 added 'declaration' command;
wenzelm
parents: 21955
diff changeset
   167
22202
0544af1a5117 added simproc_setup;
wenzelm
parents: 22116
diff changeset
   168
(* simprocs *)
0544af1a5117 added simproc_setup;
wenzelm
parents: 22116
diff changeset
   169
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
   170
fun simproc_setup name lhss source identifier =
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56275
diff changeset
   171
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
   172
  |> ML_Context.expression (Input.range_of source) "proc"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
   173
    "Morphism.morphism -> Proof.context -> cterm -> thm option"
42464
ae16b8abf1a8 proper binding/report of defined simprocs;
wenzelm
parents: 42425
diff changeset
   174
    ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   175
      \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   176
      \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
22202
0544af1a5117 added simproc_setup;
wenzelm
parents: 22116
diff changeset
   177
  |> Context.proof_map;
0544af1a5117 added simproc_setup;
wenzelm
parents: 22116
diff changeset
   178
0544af1a5117 added simproc_setup;
wenzelm
parents: 22116
diff changeset
   179
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   180
(* goals *)
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   181
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   182
fun goal opt_chain goal stmt int =
29383
223f18cfbb32 qed/after_qed: singleton result;
wenzelm
parents: 29360
diff changeset
   183
  opt_chain #> goal NONE (K I) stmt int;
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   184
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36178
diff changeset
   185
val have = goal I Proof.have_cmd;
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36178
diff changeset
   186
val hence = goal Proof.chain Proof.have_cmd;
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36178
diff changeset
   187
val show = goal I Proof.show_cmd;
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36178
diff changeset
   188
val thus = goal Proof.chain Proof.show_cmd;
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   189
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   190
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   191
(* local endings *)
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   192
29383
223f18cfbb32 qed/after_qed: singleton result;
wenzelm
parents: 29360
diff changeset
   193
fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31819
diff changeset
   194
val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
29383
223f18cfbb32 qed/after_qed: singleton result;
wenzelm
parents: 29360
diff changeset
   195
val local_default_proof = Toplevel.proof Proof.local_default_proof;
223f18cfbb32 qed/after_qed: singleton result;
wenzelm
parents: 29360
diff changeset
   196
val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
223f18cfbb32 qed/after_qed: singleton result;
wenzelm
parents: 29360
diff changeset
   197
val local_done_proof = Toplevel.proof Proof.local_done_proof;
223f18cfbb32 qed/after_qed: singleton result;
wenzelm
parents: 29360
diff changeset
   198
val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   199
27562
bcb01eb565ee removed obsolete history commands;
wenzelm
parents: 27493
diff changeset
   200
val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   201
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   202
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   203
(* global endings *)
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   204
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   205
fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
49012
8686c36fa27d refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents: 48918
diff changeset
   206
val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   207
val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   208
val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   209
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   210
val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   211
28375
c879d88d038a eliminated polymorphic equality;
wenzelm
parents: 28290
diff changeset
   212
val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1);
21350
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   213
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   214
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   215
(* common endings *)
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   216
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   217
fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   218
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   219
val default_proof = local_default_proof o global_default_proof;
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   220
val immediate_proof = local_immediate_proof o global_immediate_proof;
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   221
val done_proof = local_done_proof o global_done_proof;
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   222
val skip_proof = local_skip_proof o global_skip_proof;
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   223
6e58289b6685 incorporated IsarThy into IsarCmd;
wenzelm
parents: 21003
diff changeset
   224
26489
e83dc4bb9ab4 removed obsolete use_XXX;
wenzelm
parents: 26463
diff changeset
   225
(* diagnostic ML evaluation *)
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   226
37305
9763792e4ac7 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents: 37216
diff changeset
   227
structure Diag_State = Proof_Data
9763792e4ac7 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents: 37216
diff changeset
   228
(
9763792e4ac7 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents: 37216
diff changeset
   229
  type T = Toplevel.state;
9763792e4ac7 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents: 37216
diff changeset
   230
  fun init _ = Toplevel.toplevel;
9763792e4ac7 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents: 37216
diff changeset
   231
);
9763792e4ac7 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents: 37216
diff changeset
   232
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 53171
diff changeset
   233
fun ml_diag verbose source = Toplevel.keep (fn state =>
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   234
  let
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   235
    val opt_ctxt =
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   236
      try Toplevel.generic_theory_of state
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   237
      |> Option.map (Context.proof_of #> Diag_State.put state);
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   238
    val flags = ML_Compiler.verbose verbose ML_Compiler.flags;
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56278
diff changeset
   239
  in ML_Context.eval_source_in opt_ctxt flags source end);
37305
9763792e4ac7 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents: 37216
diff changeset
   240
48776
37cd53e69840 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents: 47815
diff changeset
   241
val diag_state = Diag_State.get;
60094
96a4765ba7d1 explicit error for Toplevel.proof_of;
wenzelm
parents: 60093
diff changeset
   242
val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
37305
9763792e4ac7 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents: 37216
diff changeset
   243
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52549
diff changeset
   244
val _ = Theory.setup
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56158
diff changeset
   245
  (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52549
diff changeset
   246
    (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56158
diff changeset
   247
   ML_Antiquotation.value (Binding.qualify true "Isar" @{binding goal})
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 52549
diff changeset
   248
    (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   249
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   250
56868
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   251
(* theorems of theory or proof context *)
17066
b53f050bc37d back: removed ill-defined '!' option;
wenzelm
parents: 16812
diff changeset
   252
56868
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   253
fun pretty_theorems verbose st =
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   254
  if Toplevel.is_proof st then
59917
9830c944670f more uniform "verbose" option to print name space;
wenzelm
parents: 59210
diff changeset
   255
    Proof_Context.pretty_local_facts verbose (Toplevel.context_of st)
56868
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   256
  else
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   257
    let
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   258
      val thy = Toplevel.theory_of st;
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   259
      val prev_thys =
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   260
        (case Toplevel.previous_context_of st of
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   261
          SOME prev => [Proof_Context.theory_of prev]
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   262
        | NONE => Theory.parents_of thy);
b5fb264d53ba clarified print operations for "terms" and "theorems";
wenzelm
parents: 56334
diff changeset
   263
    in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
9513
8531c18d9181 unknown_theory/proof/context;
wenzelm
parents: 9454
diff changeset
   264
12060
f85eddf6a4fb added print_locales, print_locale;
wenzelm
parents: 12055
diff changeset
   265
19268
5a575522fd26 added print_stmts;
wenzelm
parents: 19057
diff changeset
   266
(* print theorems, terms, types etc. *)
5a575522fd26 added print_stmts;
wenzelm
parents: 19057
diff changeset
   267
19385
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   268
local
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   269
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   270
fun string_of_stmts ctxt args =
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   271
  Attrib.eval_thms ctxt args
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   272
  |> map (Element.pretty_statement ctxt Thm.theoremK)
19385
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   273
  |> Pretty.chunks2 |> Pretty.string_of;
5880
feec44106a8e add print_theorems;
wenzelm
parents: 5831
diff changeset
   274
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   275
fun string_of_thms ctxt args =
51583
9100c8e66b69 item markup for Proof_Context.pretty_fact;
wenzelm
parents: 50737
diff changeset
   276
  Pretty.string_of (Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args));
5895
457b42674b57 added print_thm;
wenzelm
parents: 5880
diff changeset
   277
19385
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   278
fun string_of_prfs full state arg =
32859
204f749f35a9 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents: 32804
diff changeset
   279
  Pretty.string_of
204f749f35a9 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents: 32804
diff changeset
   280
    (case arg of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   281
      NONE =>
12125
316d11f760f7 Commands prf and full_prf can now also be used to display proof term
berghofe
parents: 12069
diff changeset
   282
        let
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   283
          val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   284
          val thy = Proof_Context.theory_of ctxt;
28814
463c9e9111ae clarified Thm.proof_body_of vs. Thm.proof_of;
wenzelm
parents: 28799
diff changeset
   285
          val prf = Thm.proof_of thm;
17066
b53f050bc37d back: removed ill-defined '!' option;
wenzelm
parents: 16812
diff changeset
   286
          val prop = Thm.full_prop_of thm;
32859
204f749f35a9 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents: 32804
diff changeset
   287
          val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
12125
316d11f760f7 Commands prf and full_prf can now also be used to display proof term
berghofe
parents: 12069
diff changeset
   288
        in
33388
d64545e6cba5 modernized structure Proof_Syntax;
wenzelm
parents: 33369
diff changeset
   289
          Proof_Syntax.pretty_proof ctxt
17066
b53f050bc37d back: removed ill-defined '!' option;
wenzelm
parents: 16812
diff changeset
   290
            (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
12125
316d11f760f7 Commands prf and full_prf can now also be used to display proof term
berghofe
parents: 12069
diff changeset
   291
        end
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   292
    | SOME srcs =>
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   293
        let val ctxt = Toplevel.context_of state
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   294
        in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   295
        |> Pretty.chunks);
11524
197f2e14a714 Added functions for printing primitive proof terms.
berghofe
parents: 11017
diff changeset
   296
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   297
fun string_of_prop ctxt s =
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   298
  let
24508
c8b82fec6447 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24314
diff changeset
   299
    val prop = Syntax.read_prop ctxt s;
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 26694
diff changeset
   300
    val ctxt' = Variable.auto_fixes prop ctxt;
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 26694
diff changeset
   301
  in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   302
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   303
fun string_of_term ctxt s =
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   304
  let
24508
c8b82fec6447 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24314
diff changeset
   305
    val t = Syntax.read_term ctxt s;
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   306
    val T = Term.type_of t;
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 26694
diff changeset
   307
    val ctxt' = Variable.auto_fixes t ctxt;
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   308
  in
19385
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   309
    Pretty.string_of
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 26694
diff changeset
   310
      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 26694
diff changeset
   311
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
9128
35abf6308ab0 rearranged print commands;
wenzelm
parents: 9009
diff changeset
   312
  end;
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   313
48792
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   314
fun string_of_type ctxt (s, NONE) =
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   315
      let val T = Syntax.read_typ ctxt s
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   316
      in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   317
  | string_of_type ctxt (s1, SOME s2) =
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   318
      let
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   319
        val ctxt' = Config.put show_sorts true ctxt;
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   320
        val raw_T = Syntax.parse_typ ctxt' s1;
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   321
        val S = Syntax.read_sort ctxt' s2;
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   322
        val T =
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   323
          Syntax.check_term ctxt'
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   324
            (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S)))
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   325
          |> Logic.dest_type;
4aa5b965f70e support for 'typ' with explicit sort constraint;
wenzelm
parents: 48776
diff changeset
   326
      in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end;
9128
35abf6308ab0 rearranged print commands;
wenzelm
parents: 9009
diff changeset
   327
23935
2a4e42ec9a54 PrintMode.with_modes;
wenzelm
parents: 23897
diff changeset
   328
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   329
  Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
19385
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   330
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   331
in
9128
35abf6308ab0 rearranged print commands;
wenzelm
parents: 9009
diff changeset
   332
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   333
val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   334
val print_thms = print_item (string_of_thms o Toplevel.context_of);
19385
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   335
val print_prfs = print_item o string_of_prfs;
38331
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   336
val print_prop = print_item (string_of_prop o Toplevel.context_of);
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   337
val print_term = print_item (string_of_term o Toplevel.context_of);
6e72f31999ac prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents: 38139
diff changeset
   338
val print_type = print_item (string_of_type o Toplevel.context_of);
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   339
19385
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   340
end;
c0f2f8224ea8 print_term etc.: actually observe print mode in final output;
wenzelm
parents: 19268
diff changeset
   341
5831
996361157cfb Non-logical toplevel commands.
wenzelm
parents:
diff changeset
   342
end;