doc-src/Codegen/Setup.thy
author wenzelm
Mon Aug 27 23:00:38 2012 +0200 (2012-08-27)
changeset 48951 b9238cbcdd41
parent 48891 doc-src/Codegen/Thy/Setup.thy@c0eafbd55de3
permissions -rw-r--r--
more standard document preparation within session context;
haftmann@28213
     1
theory Setup
haftmann@39066
     2
imports
haftmann@39066
     3
  Complex_Main
haftmann@46517
     4
  "~~/src/HOL/Library/Dlist"
haftmann@46517
     5
  "~~/src/HOL/Library/RBT"
haftmann@46517
     6
  "~~/src/HOL/Library/Mapping"
haftmann@28213
     7
begin
haftmann@28213
     8
wenzelm@48951
     9
(* FIXME avoid writing into source directory *)
wenzelm@48951
    10
ML {*
wenzelm@48951
    11
  Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples"))
wenzelm@48951
    12
*}
wenzelm@48951
    13
wenzelm@48951
    14
ML_file "../antiquote_setup.ML"
wenzelm@48951
    15
ML_file "../more_antiquote.ML"
wenzelm@48891
    16
haftmann@38503
    17
setup {*
wenzelm@43564
    18
  Antiquote_Setup.setup #>
wenzelm@43564
    19
  More_Antiquote.setup #>
haftmann@38503
    20
let
haftmann@38503
    21
  val typ = Simple_Syntax.read_typ;
haftmann@38503
    22
in
wenzelm@42293
    23
  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293
    24
   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
wenzelm@42293
    25
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
wenzelm@42293
    26
  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293
    27
   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
wenzelm@42293
    28
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
haftmann@38503
    29
end
haftmann@38503
    30
*}
haftmann@38503
    31
haftmann@34071
    32
setup {* Code_Target.set_default_code_width 74 *}
haftmann@34071
    33
wenzelm@42669
    34
declare [[names_unique = false]]
haftmann@28213
    35
haftmann@28213
    36
end
haftmann@46517
    37