src/Doc/more_antiquote.ML
author wenzelm
Tue, 31 Mar 2015 22:31:05 +0200
changeset 59886 e0dc738eb08c
parent 56061 564a7bee8652
child 60697 e266d5463e9d
permissions -rw-r--r--
support for explicit scope of private entries;
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
56061
564a7bee8652 modernized setup;
wenzelm
parents: 54889
diff changeset
     4
More antiquotations (depending on Isabelle/HOL).
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     5
*)
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     6
56061
564a7bee8652 modernized setup;
wenzelm
parents: 54889
diff changeset
     7
structure More_Antiquote : sig end =
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     8
struct
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     9
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    10
(* code theorem antiquotation *)
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    11
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    12
local
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    13
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    14
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    15
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    16
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    17
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    18
fun no_vars ctxt thm =
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    19
  let
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    20
    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
    21
    val ((_, [thm]), _) = Variable.import true [thm] ctxt';
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    22
  in thm end;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    23
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    24
fun pretty_code_thm src ctxt raw_const =
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    25
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39540
diff changeset
    26
    val thy = Proof_Context.theory_of ctxt;
31156
90fed3d4430f merged module code_unit.ML into code.ML
haftmann
parents: 31143
diff changeset
    27
    val const = Code.check_const thy raw_const;
39540
49c319fff40c adjusted
haftmann
parents: 39478
diff changeset
    28
    val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
29874
0b92f68124e8 display code theorems with HOL equality
haftmann
parents: 29619
diff changeset
    29
    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
    30
    val thms = Code_Preproc.cert eqngr const
35246
bcbb5ba7dbbc adjusted to changes in cs b987b803616d
haftmann
parents: 34896
diff changeset
    31
      |> Code.equations_of_cert thy
34896
a22b09addd78 adjusted to changes in code equation administration
haftmann
parents: 34072
diff changeset
    32
      |> snd
54889
4121d64fde90 explicit distinction between empty code equations and no code equations, including convenient declaration attributes
haftmann
parents: 51685
diff changeset
    33
      |> these
35246
bcbb5ba7dbbc adjusted to changes in cs b987b803616d
haftmann
parents: 34896
diff changeset
    34
      |> 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
    35
      |> 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
    36
  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
    37
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    38
in
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    39
56061
564a7bee8652 modernized setup;
wenzelm
parents: 54889
diff changeset
    40
val _ =
564a7bee8652 modernized setup;
wenzelm
parents: 54889
diff changeset
    41
  Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
564a7bee8652 modernized setup;
wenzelm
parents: 54889
diff changeset
    42
    (fn {source, context, ...} => pretty_code_thm source context));
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    43
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    44
end;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    45
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    46
end;