src/Doc/more_antiquote.ML
author wenzelm
Sat, 25 May 2013 17:40:44 +0200
changeset 52147 9943f8067f11
parent 51685 385ef6706252
child 54889 4121d64fde90
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48985
5386df44a037 renamed doc-src to src/Doc;
wenzelm
parents: 43564
diff changeset
     1
(*  Title:      Doc/more_antiquote.ML
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     3
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     4
More antiquotations.
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     5
*)
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     6
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     7
signature MORE_ANTIQUOTE =
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     8
sig
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42361
diff changeset
     9
  val setup: theory -> theory
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    10
end;
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    11
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    12
structure More_Antiquote : MORE_ANTIQUOTE =
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    13
struct
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    14
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    15
(* code theorem antiquotation *)
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    16
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    17
local
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    18
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    19
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    20
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    21
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    22
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    23
fun no_vars ctxt thm =
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    24
  let
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    25
    val ctxt' = Variable.set_body false ctxt;
31794
71af1fd6a5e4 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents: 31156
diff changeset
    26
    val ((_, [thm]), _) = Variable.import true [thm] ctxt';
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    27
  in thm end;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    28
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    29
fun pretty_code_thm src ctxt raw_const =
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    30
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39540
diff changeset
    31
    val thy = Proof_Context.theory_of ctxt;
31156
90fed3d4430f merged module code_unit.ML into code.ML
haftmann
parents: 31143
diff changeset
    32
    val const = Code.check_const thy raw_const;
39540
49c319fff40c adjusted
haftmann
parents: 39478
diff changeset
    33
    val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
29874
0b92f68124e8 display code theorems with HOL equality
haftmann
parents: 29619
diff changeset
    34
    fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
34896
a22b09addd78 adjusted to changes in code equation administration
haftmann
parents: 34072
diff changeset
    35
    val thms = Code_Preproc.cert eqngr const
35246
bcbb5ba7dbbc adjusted to changes in cs b987b803616d
haftmann
parents: 34896
diff changeset
    36
      |> Code.equations_of_cert thy
34896
a22b09addd78 adjusted to changes in code equation administration
haftmann
parents: 34072
diff changeset
    37
      |> snd
35246
bcbb5ba7dbbc adjusted to changes in cs b987b803616d
haftmann
parents: 34896
diff changeset
    38
      |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
51685
385ef6706252 more standard module name Axclass (according to file name);
wenzelm
parents: 48985
diff changeset
    39
      |> map (holize o no_vars ctxt o Axclass.overload thy);
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 37216
diff changeset
    40
  in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    41
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    42
in
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    43
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42361
diff changeset
    44
val setup =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42361
diff changeset
    45
  Thy_Output.antiquotation @{binding code_thms} Args.term
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42361
diff changeset
    46
    (fn {source, context, ...} => pretty_code_thm source context);
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    47
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    48
end;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    49
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    50
end;