doc-src/Classes/Thy/Setup.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 38321 7edf0ab9d5cb
child 42224 578a51fae383
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
haftmann@28565
     1
theory Setup
wenzelm@41413
     2
imports Main "~~/src/HOL/Library/Code_Integer"
haftmann@28565
     3
uses
haftmann@38321
     4
  "../../antiquote_setup.ML"
haftmann@38321
     5
  "../../more_antiquote.ML"
haftmann@28565
     6
begin
haftmann@28565
     7
haftmann@34071
     8
setup {* Code_Target.set_default_code_width 74 *}
haftmann@28565
     9
haftmann@28565
    10
syntax
haftmann@28565
    11
  "_alpha" :: "type"  ("\<alpha>")
haftmann@28565
    12
  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
haftmann@28565
    13
  "_beta" :: "type"  ("\<beta>")
haftmann@28565
    14
  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
haftmann@28565
    15
haftmann@28565
    16
parse_ast_translation {*
haftmann@28565
    17
  let
haftmann@28565
    18
    fun alpha_ast_tr [] = Syntax.Variable "'a"
haftmann@28565
    19
      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
haftmann@28565
    20
    fun alpha_ofsort_ast_tr [ast] =
wenzelm@35113
    21
      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
haftmann@28565
    22
      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
haftmann@28565
    23
    fun beta_ast_tr [] = Syntax.Variable "'b"
haftmann@28565
    24
      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
haftmann@28565
    25
    fun beta_ofsort_ast_tr [ast] =
wenzelm@35113
    26
      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
haftmann@28565
    27
      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
wenzelm@35113
    28
  in
wenzelm@35113
    29
   [(@{syntax_const "_alpha"}, alpha_ast_tr),
wenzelm@35113
    30
    (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
wenzelm@35113
    31
    (@{syntax_const "_beta"}, beta_ast_tr),
wenzelm@35113
    32
    (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
wenzelm@35113
    33
  end
haftmann@28565
    34
*}
haftmann@28565
    35
haftmann@28565
    36
end