# HG changeset patch # User wenzelm # Date 1451397495 -3600 # Node ID 301833d9013aeb5c5740757241825851a1584c8d # Parent 38b73f7940af1764e1aa3e42e54ee8033fdea9dc former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; uniform syntax for Pure.imp; removed obsolete "HTML" syntax; diff -r 38b73f7940af -r 301833d9013a src/Pure/General/print_mode.ML --- a/src/Pure/General/print_mode.ML Mon Dec 28 23:13:33 2015 +0100 +++ b/src/Pure/General/print_mode.ML Tue Dec 29 14:58:15 2015 +0100 @@ -18,6 +18,7 @@ sig include BASIC_PRINT_MODE val input: string + val ASCII: string val internal: string val setmp: string list -> ('a -> 'b) -> 'a -> 'b val with_modes: string list -> ('a -> 'b) -> 'a -> 'b @@ -28,6 +29,7 @@ struct val input = "input"; +val ASCII = "ASCII"; val internal = "internal"; val print_mode = Unsynchronized.ref ([]: string list); diff -r 38b73f7940af -r 301833d9013a src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Mon Dec 28 23:13:33 2015 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Tue Dec 29 14:58:15 2015 +0100 @@ -46,8 +46,8 @@ |> Sign.add_types_global [(Binding.make ("proof", @{here}), 0, NoSyn)] |> fold (snd oo Sign.declare_const_global) - [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)), - ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)), + [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ \/ _)", [4, 5], 4)), + ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ \/ _)", [4, 5], 4)), ((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn), ((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn), ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn), @@ -58,17 +58,17 @@ [Binding.make ("param", @{here}), Binding.make ("params", @{here})] |> Sign.add_syntax Syntax.mode_default - [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), + [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)), ("", paramT --> paramT, Delimfix "'(_')"), ("", idtT --> paramsT, Delimfix "_"), ("", paramT --> paramsT, Delimfix "_")] - |> Sign.add_syntax (Symbol.xsymbolsN, true) - [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), - (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4)), - (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4))] + |> Sign.add_syntax (Print_Mode.ASCII, true) + [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), + (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), + (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4))] |> Sign.add_trrules (map Syntax.Parse_Print_Rule [(Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam0") diff -r 38b73f7940af -r 301833d9013a src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Dec 28 23:13:33 2015 +0100 +++ b/src/Pure/pure_thy.ML Tue Dec 29 14:58:15 2015 +0100 @@ -108,12 +108,12 @@ ("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"), ("", typ "type => types", Delimfix "_"), ("_types", typ "type => types => types", Delimfix "_,/ _"), - ("\\<^type>fun", typ "type => type => type", Mixfix ("(_/ => _)", [1, 0], 0)), - ("_bracket", typ "types => type => type", Mixfix ("([_]/ => _)", [0, 0], 0)), + ("\\<^type>fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), + ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("", typ "type => type", Delimfix "'(_')"), ("\\<^type>dummy", typ "type", Delimfix "'_"), ("_type_prop", typ "'a", NoSyn), - ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), + ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), ("_abs", typ "'a", NoSyn), ("", typ "'a => args", Delimfix "_"), ("_args", typ "'a => args => args", Delimfix "_,/ _"), @@ -131,18 +131,18 @@ ("", typ "id_position => aprop", Delimfix "_"), ("", typ "longid_position => aprop", Delimfix "_"), ("", typ "var_position => aprop", Delimfix "_"), - ("_DDDOT", typ "aprop", Delimfix "..."), + ("_DDDOT", typ "aprop", Delimfix "\\"), ("_aprop", typ "aprop => prop", Delimfix "PROP _"), ("_asm", typ "prop => asms", Delimfix "_"), ("_asms", typ "prop => asms => asms", Delimfix "_;/ _"), - ("_bigimpl", typ "asms => prop => prop", Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), + ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"), ("_mk_ofclass", typ "dummy", NoSyn), ("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"), ("", typ "id_position => logic", Delimfix "_"), ("", typ "longid_position => logic", Delimfix "_"), ("", typ "var_position => logic", Delimfix "_"), - ("_DDDOT", typ "logic", Delimfix "..."), + ("_DDDOT", typ "logic", Delimfix "\\"), ("_strip_positions", typ "'a", NoSyn), ("_position", typ "num_token => num_position", Delimfix "_"), ("_position", typ "float_token => float_position", Delimfix "_"), @@ -171,30 +171,27 @@ ("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"), ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"), ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"), - (const "Pure.imp", typ "prop => prop => prop", Delimfix "op ==>"), (const "Pure.dummy_pattern", typ "aprop", Delimfix "'_"), ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), (const "Pure.term", typ "logic => prop", Delimfix "TERM _"), (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] #> Sign.add_syntax Syntax.mode_default applC_syntax - #> Sign.add_syntax (Symbol.xsymbolsN, true) - [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), - ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), - ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), - (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\", 2)), - (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), - (const "Pure.imp", typ "prop => prop => prop", Infixr ("\\", 1)), - ("_DDDOT", typ "aprop", Delimfix "\\"), - ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), - ("_DDDOT", typ "logic", Delimfix "\\")] + #> Sign.add_syntax (Print_Mode.ASCII, true) + [(tycon "fun", typ "type => type => type", Mixfix ("(_/ => _)", [1, 0], 0)), + ("_bracket", typ "types => type => type", Mixfix ("([_]/ => _)", [0, 0], 0)), + ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), + (const "Pure.eq", typ "'a => 'a => prop", Infix ("==", 2)), + (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3!!_./ _)", [0, 0], 0)), + (const "Pure.imp", typ "prop => prop => prop", Infixr ("==>", 1)), + ("_DDDOT", typ "aprop", Delimfix "..."), + ("_bigimpl", typ "asms => prop => prop", Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), + ("_DDDOT", typ "logic", Delimfix "...")] #> Sign.add_syntax ("", false) [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))] - #> Sign.add_syntax ("HTML", false) - [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3))] #> Sign.add_consts - [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("==", 2)), - (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), - (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("!!", 0, 0)), + [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\\", 2)), + (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\\", 1)), + (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\\", 0, 0)), (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn), (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn), (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]