former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
authorwenzelm
Tue Dec 29 14:58:15 2015 +0100 (2015-12-29)
changeset 61957301833d9013a
parent 61956 38b73f7940af
child 61958 0a5dd617a88c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
uniform syntax for Pure.imp;
removed obsolete "HTML" syntax;
src/Pure/General/print_mode.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/General/print_mode.ML	Mon Dec 28 23:13:33 2015 +0100
     1.2 +++ b/src/Pure/General/print_mode.ML	Tue Dec 29 14:58:15 2015 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4  sig
     1.5    include BASIC_PRINT_MODE
     1.6    val input: string
     1.7 +  val ASCII: string
     1.8    val internal: string
     1.9    val setmp: string list -> ('a -> 'b) -> 'a -> 'b
    1.10    val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
    1.11 @@ -28,6 +29,7 @@
    1.12  struct
    1.13  
    1.14  val input = "input";
    1.15 +val ASCII = "ASCII";
    1.16  val internal = "internal";
    1.17  
    1.18  val print_mode = Unsynchronized.ref ([]: string list);
     2.1 --- a/src/Pure/Proof/proof_syntax.ML	Mon Dec 28 23:13:33 2015 +0100
     2.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Dec 29 14:58:15 2015 +0100
     2.3 @@ -46,8 +46,8 @@
     2.4    |> Sign.add_types_global
     2.5      [(Binding.make ("proof", @{here}), 0, NoSyn)]
     2.6    |> fold (snd oo Sign.declare_const_global)
     2.7 -    [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
     2.8 -     ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
     2.9 +    [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
    2.10 +     ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
    2.11       ((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn),
    2.12       ((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn),
    2.13       ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
    2.14 @@ -58,17 +58,17 @@
    2.15      [Binding.make ("param", @{here}),
    2.16       Binding.make ("params", @{here})]
    2.17    |> Sign.add_syntax Syntax.mode_default
    2.18 -    [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    2.19 +    [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
    2.20       ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    2.21       ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    2.22       ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
    2.23       ("", paramT --> paramT, Delimfix "'(_')"),
    2.24       ("", idtT --> paramsT, Delimfix "_"),
    2.25       ("", paramT --> paramsT, Delimfix "_")]
    2.26 -  |> Sign.add_syntax (Symbol.xsymbolsN, true)
    2.27 -    [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
    2.28 -     (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
    2.29 -     (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
    2.30 +  |> Sign.add_syntax (Print_Mode.ASCII, true)
    2.31 +    [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    2.32 +     (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    2.33 +     (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4))]
    2.34    |> Sign.add_trrules (map Syntax.Parse_Print_Rule
    2.35      [(Ast.mk_appl (Ast.Constant "_Lam")
    2.36          [Ast.mk_appl (Ast.Constant "_Lam0")
     3.1 --- a/src/Pure/pure_thy.ML	Mon Dec 28 23:13:33 2015 +0100
     3.2 +++ b/src/Pure/pure_thy.ML	Tue Dec 29 14:58:15 2015 +0100
     3.3 @@ -108,12 +108,12 @@
     3.4      ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
     3.5      ("",            typ "type => types",               Delimfix "_"),
     3.6      ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
     3.7 -    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ => _)", [1, 0], 0)),
     3.8 -    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ => _)", [0, 0], 0)),
     3.9 +    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    3.10 +    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    3.11      ("",            typ "type => type",                Delimfix "'(_')"),
    3.12      ("\\<^type>dummy", typ "type",                     Delimfix "'_"),
    3.13      ("_type_prop",  typ "'a",                          NoSyn),
    3.14 -    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
    3.15 +    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    3.16      ("_abs",        typ "'a",                          NoSyn),
    3.17      ("",            typ "'a => args",                  Delimfix "_"),
    3.18      ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
    3.19 @@ -131,18 +131,18 @@
    3.20      ("",            typ "id_position => aprop",        Delimfix "_"),
    3.21      ("",            typ "longid_position => aprop",    Delimfix "_"),
    3.22      ("",            typ "var_position => aprop",       Delimfix "_"),
    3.23 -    ("_DDDOT",      typ "aprop",                       Delimfix "..."),
    3.24 +    ("_DDDOT",      typ "aprop",                       Delimfix "\\<dots>"),
    3.25      ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
    3.26      ("_asm",        typ "prop => asms",                Delimfix "_"),
    3.27      ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
    3.28 -    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
    3.29 +    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    3.30      ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    3.31      ("_mk_ofclass", typ "dummy",                       NoSyn),
    3.32      ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
    3.33      ("",            typ "id_position => logic",        Delimfix "_"),
    3.34      ("",            typ "longid_position => logic",    Delimfix "_"),
    3.35      ("",            typ "var_position => logic",       Delimfix "_"),
    3.36 -    ("_DDDOT",      typ "logic",                       Delimfix "..."),
    3.37 +    ("_DDDOT",      typ "logic",                       Delimfix "\\<dots>"),
    3.38      ("_strip_positions", typ "'a", NoSyn),
    3.39      ("_position",   typ "num_token => num_position",   Delimfix "_"),
    3.40      ("_position",   typ "float_token => float_position", Delimfix "_"),
    3.41 @@ -171,30 +171,27 @@
    3.42      ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
    3.43      ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
    3.44      ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
    3.45 -    (const "Pure.imp",  typ "prop => prop => prop",     Delimfix "op ==>"),
    3.46      (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
    3.47      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
    3.48      (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
    3.49      (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
    3.50    #> Sign.add_syntax Syntax.mode_default applC_syntax
    3.51 -  #> Sign.add_syntax (Symbol.xsymbolsN, true)
    3.52 -   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    3.53 -    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    3.54 -    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    3.55 -    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
    3.56 -    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    3.57 -    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
    3.58 -    ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
    3.59 -    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    3.60 -    ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
    3.61 +  #> Sign.add_syntax (Print_Mode.ASCII, true)
    3.62 +   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ => _)", [1, 0], 0)),
    3.63 +    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ => _)", [0, 0], 0)),
    3.64 +    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3%_./ _)", [0, 3], 3)),
    3.65 +    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("==", 2)),
    3.66 +    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3!!_./ _)", [0, 0], 0)),
    3.67 +    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("==>", 1)),
    3.68 +    ("_DDDOT",            typ "aprop",                  Delimfix "..."),
    3.69 +    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
    3.70 +    ("_DDDOT",            typ "logic",                  Delimfix "...")]
    3.71    #> Sign.add_syntax ("", false)
    3.72     [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
    3.73 -  #> Sign.add_syntax ("HTML", false)
    3.74 -   [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
    3.75    #> Sign.add_consts
    3.76 -   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("==", 2)),
    3.77 -    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    3.78 -    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    3.79 +   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
    3.80 +    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
    3.81 +    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\\<And>", 0, 0)),
    3.82      (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
    3.83      (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
    3.84      (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]