# HG changeset patch # User wenzelm # Date 1459279049 -7200 # Node ID d09d71223e7a7f923c3b4ce4e10ff4a1c60d11e3 # Parent 24e2b098bf4436c3a5fdd41563cdaca31f156de3 more position information for type mixfix; diff -r 24e2b098bf44 -r d09d71223e7a src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Mar 29 21:17:29 2016 +0200 @@ -87,29 +87,31 @@ type atom_pool = ((string * int) * int list) list +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range) + fun add_wacky_syntax ctxt = let val name_of = fst o dest_Const val thy = Proof_Context.theory_of ctxt val (unrep_s, thy) = thy |> Sign.declare_const_global ((@{binding nitpick_unrep}, @{typ 'a}), - Mixfix (unrep_mixfix (), [], 1000)) + mixfix (unrep_mixfix (), [], 1000)) |>> name_of val (maybe_s, thy) = thy |> Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), - Mixfix (maybe_mixfix (), [1000], 1000)) + mixfix (maybe_mixfix (), [1000], 1000)) |>> name_of val (abs_s, thy) = thy |> Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}), - Mixfix (abs_mixfix (), [40], 40)) + mixfix (abs_mixfix (), [40], 40)) |>> name_of val (base_s, thy) = thy |> Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}), - Mixfix (base_mixfix (), [1000], 1000)) + mixfix (base_mixfix (), [1000], 1000)) |>> name_of val (step_s, thy) = thy |> Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}), - Mixfix (step_mixfix (), [1000], 1000)) + mixfix (step_mixfix (), [1000], 1000)) |>> name_of in (((unrep_s, maybe_s, abs_s), (base_s, step_s)), diff -r 24e2b098bf44 -r d09d71223e7a src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Mar 29 21:17:29 2016 +0200 @@ -1959,8 +1959,8 @@ val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr val setT = HOLogic.mk_setT T val elems = HOLogic.mk_set T ts - val ([dots], ctxt') = - Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt + val ([dots], ctxt') = ctxt + |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Delimfix (\...\, Position.no_range))] (* check expected values *) val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT) val () = diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/General/input.ML --- a/src/Pure/General/input.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/General/input.ML Tue Mar 29 21:17:29 2016 +0200 @@ -15,6 +15,7 @@ val string: string -> source val source_explode: source -> Symbol_Pos.T list val source_content: source -> string + val equal_content: source * source -> bool end; structure Input: INPUT = @@ -38,6 +39,8 @@ val source_content = source_explode #> Symbol_Pos.content; +val equal_content = (op =) o apply2 source_content; + end; end; diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Isar/class.ML Tue Mar 29 21:17:29 2016 +0200 @@ -616,8 +616,10 @@ fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case instantiation_param lthy b of SOME c => - if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) - else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs) + if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs) + else + error ("Illegal mixfix syntax for overloaded constant " ^ quote c ^ + Position.here (Mixfix.pos_of mx)) | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Isar/expression.ML Tue Mar 29 21:17:29 2016 +0200 @@ -85,8 +85,11 @@ [] => () | dups => error (message ^ commas dups)); - fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso - (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression")); + fun parm_eq ((p1, mx1), (p2, mx2)) = + p1 = p2 andalso + (Mixfix.equal (mx1, mx2) orelse + error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^ + Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); fun params_inst (loc, (prfx, Positional insts)) = diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Isar/generic_target.ML Tue Mar 29 21:17:29 2016 +0200 @@ -103,14 +103,17 @@ warning ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^ - (if mx = NoSyn then "" - else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))) + (if Mixfix.is_empty mx then "" + else + "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx) ^ + Position.here (Mixfix.pos_of mx))) else (); NoSyn); fun check_mixfix_global (b, no_params) mx = - if no_params orelse mx = NoSyn then mx - else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ - Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); + if no_params orelse Mixfix.is_empty mx then mx + else + (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ + Pretty.string_of (Mixfix.pretty_mixfix mx) ^ Position.here (Mixfix.pos_of mx)); NoSyn); fun same_const (Const (c, _), Const (c', _)) = c = c' | same_const (t $ _, t' $ _) = same_const (t, t') diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Isar/overloading.ML Tue Mar 29 21:17:29 2016 +0200 @@ -158,9 +158,11 @@ fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case operation lthy b of SOME (c, (v, checked)) => - if mx <> NoSyn - then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) - else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) + if Mixfix.is_empty mx then + lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) + else + error ("Illegal mixfix syntax for overloaded constant " ^ quote c ^ + Position.here (Mixfix.pos_of mx)) | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Isar/parse.ML Tue Mar 29 21:17:29 2016 +0200 @@ -317,22 +317,33 @@ local -val mfix = string -- - !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- - Scan.optional nat 1000) >> (Mixfix o Scan.triple2); +val mfix = + input string -- + !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000) + >> (fn (sy, (ps, p)) => Mixfix (sy, ps, p, Position.no_range)); + +val infx = + $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => Infix (sy, p, Position.no_range))); -val infx = $$$ "infix" |-- !!! (string -- nat >> Infix); -val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl); -val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr); -val strcture = $$$ "structure" >> K Structure; +val infxl = + $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => Infixl (sy, p, Position.no_range))); + +val infxr = + $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => Infixr (sy, p, Position.no_range))); -val binder = $$$ "binder" |-- - !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n)))) - >> (Binder o Scan.triple2); +val strcture = $$$ "structure" >> K (Structure Position.no_range); + +val binder = + $$$ "binder" |-- + !!! (input string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n)))) + >> (fn (sy, (p, q)) => Binder (sy, p, q, Position.no_range)); val mixfix_body = mfix || strcture || binder || infxl || infxr || infx; -fun annotation guard body = $$$ "(" |-- guard (body --| $$$ ")"); +fun annotation guard body = + Scan.trace ($$$ "(" |-- guard (body --| $$$ ")")) + >> (fn (mx, toks) => Mixfix.set_range (Token.range_of toks) mx); + fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn; in diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Mar 29 21:17:29 2016 +0200 @@ -30,6 +30,7 @@ val idtT = Type ("idt", []); val aT = TFree (Name.aT, []); + (** constants for theorems and axioms **) fun add_proof_atom_consts names thy = @@ -37,8 +38,12 @@ |> Sign.root_path |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names); + (** constants for application and abstraction **) +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); +fun delimfix sy = Delimfix (Input.string sy, Position.no_range); + fun add_proof_syntax thy = thy |> Sign.root_path @@ -46,29 +51,29 @@ |> 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), ((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn), ((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn), - ((Binding.make ("MinProof", @{here}), proofT), Delimfix "?")] + ((Binding.make ("MinProof", @{here}), proofT), delimfix "?")] |> Sign.add_nonterminals_global [Binding.make ("param", @{here}), Binding.make ("params", @{here})] |> Sign.add_syntax Syntax.mode_default - [("_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 "_")] + [("_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 (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))] + [("_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 24e2b098bf44 -r d09d71223e7a src/Pure/Syntax/local_syntax.ML --- a/src/Pure/Syntax/local_syntax.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Syntax/local_syntax.ML Tue Mar 29 21:17:29 2016 +0200 @@ -76,20 +76,21 @@ local -fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE +fun prep_mixfix _ _ (_, (_, _, Structure _)) = NONE | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl)) | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl)) | prep_mixfix add mode (Fixed, (x, T, mx)) = SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx))); -fun prep_struct (Fixed, (c, _, Structure)) = SOME c - | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c) +fun prep_struct (Fixed, (c, _, Structure _)) = SOME c + | prep_struct (_, (c, _, mx as Structure _)) = + error ("Bad mixfix declaration for " ^ quote c ^ Position.here (Mixfix.pos_of mx)) | prep_struct _ = NONE; in fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) = - (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of + (case filter_out (Mixfix.is_empty o #3 o #2) raw_decls of [] => (NONE, syntax) | decls => let diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Syntax/mixfix.ML Tue Mar 29 21:17:29 2016 +0200 @@ -8,18 +8,23 @@ sig datatype mixfix = NoSyn | - Mixfix of string * int list * int | - Delimfix of string | - Infix of string * int | - Infixl of string * int | - Infixr of string * int | - Binder of string * int * int | - Structure + Mixfix of Input.source * int list * int * Position.range | + Delimfix of Input.source * Position.range | + Infix of Input.source * int * Position.range | + Infixl of Input.source * int * Position.range | + Infixr of Input.source * int * Position.range | + Binder of Input.source * int * int * Position.range | + Structure of Position.range end; signature MIXFIX = sig include BASIC_MIXFIX + val is_empty: mixfix -> bool + val equal: mixfix * mixfix -> bool + val set_range: Position.range -> mixfix -> mixfix + val range_of: mixfix -> Position.range + val pos_of: mixfix -> Position.T val pretty_mixfix: mixfix -> Pretty.T val mixfix_args: mixfix -> int val mixfixT: mixfix -> typ @@ -36,20 +41,57 @@ datatype mixfix = NoSyn | - Mixfix of string * int list * int | - Delimfix of string | - Infix of string * int | - Infixl of string * int | - Infixr of string * int | - Binder of string * int * int | - Structure; + Mixfix of Input.source * int list * int * Position.range | + Delimfix of Input.source * Position.range | + Infix of Input.source * int * Position.range | + Infixl of Input.source * int * Position.range | + Infixr of Input.source * int * Position.range | + Binder of Input.source * int * int * Position.range | + Structure of Position.range; + +fun is_empty NoSyn = true + | is_empty _ = false; + +fun equal (NoSyn, NoSyn) = true + | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) = + Input.equal_content (sy, sy') andalso ps = ps' andalso p = p' + | equal (Delimfix (sy, _), Delimfix (sy', _)) = Input.equal_content (sy, sy') + | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' + | equal (Infixl (sy, p, _), Infixl (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' + | equal (Infixr (sy, p, _), Infixr (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' + | equal (Binder (sy, p, q, _), Binder (sy', p', q', _)) = + Input.equal_content (sy, sy') andalso p = p' andalso q = q' + | equal (Structure _, Structure _) = true + | equal _ = false; + +fun set_range range mx = + (case mx of + NoSyn => NoSyn + | Mixfix (sy, ps, p, _) => Mixfix (sy, ps, p, range) + | Delimfix (sy, _) => Delimfix (sy, range) + | Infix (sy, p, _) => Infix (sy, p, range) + | Infixl (sy, p, _) => Infixl (sy, p, range) + | Infixr (sy, p, _) => Infixr (sy, p, range) + | Binder (sy, p, q, _) => Binder (sy, p, q, range) + | Structure _ => Structure range); + +fun range_of NoSyn = Position.no_range + | range_of (Mixfix (_, _, _, range)) = range + | range_of (Delimfix (_, range)) = range + | range_of (Infix (_, _, range)) = range + | range_of (Infixl (_, _, range)) = range + | range_of (Infixr (_, _, range)) = range + | range_of (Binder (_, _, _, range)) = range + | range_of (Structure range) = range; + +val pos_of = Position.set_range o range_of; (* pretty_mixfix *) local -val quoted = Pretty.quote o Pretty.str; +val quoted = Pretty.quote o Pretty.str o Input.source_content; val keyword = Pretty.keyword2; val parens = Pretty.enclose "(" ")"; val brackets = Pretty.enclose "[" "]"; @@ -58,15 +100,15 @@ in fun pretty_mixfix NoSyn = Pretty.str "" - | pretty_mixfix (Mixfix (s, ps, p)) = + | pretty_mixfix (Mixfix (s, ps, p, _)) = parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) - | pretty_mixfix (Delimfix s) = parens [quoted s] - | pretty_mixfix (Infix (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) - | pretty_mixfix (Infixl (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) - | pretty_mixfix (Infixr (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) - | pretty_mixfix (Binder (s, p1, p2)) = + | pretty_mixfix (Delimfix (s, _)) = parens [quoted s] + | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) + | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) + | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) + | pretty_mixfix (Binder (s, p1, p2, _)) = parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2]) - | pretty_mixfix Structure = parens [keyword "structure"]; + | pretty_mixfix (Structure _) = parens [keyword "structure"]; end; @@ -74,13 +116,13 @@ (* syntax specifications *) fun mixfix_args NoSyn = 0 - | mixfix_args (Mixfix (sy, _, _)) = Syntax_Ext.mfix_args sy - | mixfix_args (Delimfix sy) = Syntax_Ext.mfix_args sy - | mixfix_args (Infix (sy, _)) = 2 + Syntax_Ext.mfix_args sy - | mixfix_args (Infixl (sy, _)) = 2 + Syntax_Ext.mfix_args sy - | mixfix_args (Infixr (sy, _)) = 2 + Syntax_Ext.mfix_args sy + | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy + | mixfix_args (Delimfix (sy, _)) = Syntax_Ext.mixfix_args sy + | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy + | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy + | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy | mixfix_args (Binder _) = 1 - | mixfix_args Structure = 0; + | mixfix_args (Structure _) = 0; fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT; @@ -93,19 +135,26 @@ fun syn_ext_types type_decls = let - fun mk_infix sy ty t p1 p2 p3 = Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3); + fun mk_infix sy ty t p1 p2 p3 = + Syntax_Ext.Mfix + (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", + ty, t, [p1, p2], p3); fun mfix_of (_, _, NoSyn) = NONE - | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p)) - | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], 1000)) - | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p) - | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p) - | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p) + | mfix_of (t, ty, Mixfix (sy, ps, p, _)) = + SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p)) + | mfix_of (t, ty, Delimfix (sy, _)) = + SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000)) + | mfix_of (t, ty, Infix (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p) + | mfix_of (t, ty, Infixl (sy, p, _)) = SOME (mk_infix sy ty t p (p + 1) p) + | mfix_of (t, ty, Infixr (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) p p) | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); - fun check_args (_, ty, _) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) = + fun check_args (_, ty, mx) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) = if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then () - else Syntax_Ext.err_in_mfix "Bad number of type constructor arguments" mfix + else + error ("Bad number of type constructor arguments in mixfix annotation" ^ + Position.here (pos_of mx)) | check_args _ NONE = (); val mfix = map mfix_of type_decls; @@ -122,22 +171,30 @@ fun syn_ext_consts logical_types const_decls = let fun mk_infix sy ty c p1 p2 p3 = - [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000), - Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)]; + [Syntax_Ext.Mfix + (Symbol_Pos.explode0 "op " @ Input.source_explode sy, ty, c, [], 1000), + Syntax_Ext.Mfix + (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", + ty, c, [p1, p2], p3)]; fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = [Type ("idts", []), ty2] ---> ty3 | binder_typ c _ = error ("Bad type of binder: " ^ quote c); fun mfix_of (_, _, NoSyn) = [] - | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)] - | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], 1000)] - | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p - | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p - | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p - | mfix_of (c, ty, Binder (sy, p, q)) = - [Syntax_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)] - | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); + | mfix_of (c, ty, Mixfix (sy, ps, p, _)) = + [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p)] + | mfix_of (c, ty, Delimfix (sy, _)) = + [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000)] + | mfix_of (c, ty, Infix (sy, p, _)) = mk_infix sy ty c (p + 1) (p + 1) p + | mfix_of (c, ty, Infixl (sy, p, _)) = mk_infix sy ty c p (p + 1) p + | mfix_of (c, ty, Infixr (sy, p, _)) = mk_infix sy ty c (p + 1) p p + | mfix_of (c, ty, Binder (sy, p, q, _)) = + [Syntax_Ext.Mfix + (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)", + binder_typ c ty, (binder_name c), [0, p], q)] + | mfix_of (c, _, mx) = + error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx)); fun binder (c, _, Binder _) = SOME (binder_name c, c) | binder _ = NONE; @@ -159,4 +216,3 @@ structure Basic_Mixfix: BASIC_MIXFIX = Mixfix; open Basic_Mixfix; - diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Mar 29 21:17:29 2016 +0200 @@ -602,9 +602,9 @@ fun guess_infix (Syntax ({gram, ...}, _)) c = (case Parser.guess_infix_lr (Lazy.force gram) c of SOME (s, l, r, j) => SOME - (if l then Mixfix.Infixl (s, j) - else if r then Mixfix.Infixr (s, j) - else Mixfix.Infix (s, j)) + (if l then Mixfix.Infixl (Input.string s, j, Position.no_range) + else if r then Mixfix.Infixr (Input.string s, j, Position.no_range) + else Mixfix.Infix (Input.string s, j, Position.no_range)) | NONE => NONE); diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Tue Mar 29 21:17:29 2016 +0200 @@ -7,8 +7,7 @@ signature SYNTAX_EXT = sig val dddot_indexname: indexname - datatype mfix = Mfix of string * typ * string * int list * int - val err_in_mfix: string -> mfix -> 'a + datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int val typ_to_nonterm: typ -> string datatype xsymb = Delim of string | @@ -28,8 +27,8 @@ print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, print_rules: (Ast.ast * Ast.ast) list, print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list} - val mfix_delims: string -> string list - val mfix_args: string -> int + val mfix_args: Symbol_Pos.T list -> int + val mixfix_args: Input.source -> int val escape: string -> string val syn_ext': string list -> mfix list -> (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * @@ -112,16 +111,16 @@ (** datatype mfix **) (*Mfix (sy, ty, c, ps, p): - sy: rhs of production as symbolic string + sy: rhs of production as symbolic text ty: type description of production c: head of parse tree ps: priorities of arguments in sy p: priority of production*) -datatype mfix = Mfix of string * typ * string * int list * int; +datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int; fun err_in_mfix msg (Mfix (sy, _, const, _, _)) = - cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const); + cat_error msg ("in mixfix annotation " ^ quote (Symbol_Pos.content sy) ^ " for " ^ quote const); (* typ_to_nonterm *) @@ -140,11 +139,17 @@ local +open Basic_Symbol_Pos; + +fun scan_one pred = Scan.one (pred o Symbol_Pos.symbol); +fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol); +fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol); + val is_meta = member (op =) ["(", ")", "/", "_", "\"]; val scan_delim_char = - $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) || - Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof); + $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) || + scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof); fun read_int ["0", "0"] = ~1 | read_int cs = #1 (Library.read_int cs); @@ -152,19 +157,19 @@ val scan_sym = $$ "_" >> K (Argument ("", 0)) || $$ "\" >> K index || - $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) || + $$ "(" |-- scan_many Symbol.is_digit >> (Bg o read_int o map Symbol_Pos.symbol) || $$ ")" >> K En || $$ "/" -- $$ "/" >> K (Brk ~1) || - $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) || - Scan.many1 Symbol.is_blank >> (Space o implode) || - Scan.repeat1 scan_delim_char >> (Delim o implode); + $$ "/" |-- scan_many Symbol.is_blank >> (Brk o length) || + scan_many1 Symbol.is_blank >> (Space o Symbol_Pos.content) || + Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content); val scan_symb = scan_sym >> SOME || - $$ "'" -- Scan.one Symbol.is_blank >> K NONE; + $$ "'" -- scan_one Symbol.is_blank >> K NONE; val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); -val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs; +val read_symbs = map_filter I o the o Scan.read Symbol_Pos.stopper scan_symbs; fun unique_index xsymbs = if length (filter is_index xsymbs) <= 1 then xsymbs @@ -172,10 +177,10 @@ in -val read_mfix = unique_index o read_symbs o Symbol.explode; +val read_mfix = unique_index o read_symbs; -fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) []; val mfix_args = length o filter is_argument o read_mfix; +val mixfix_args = mfix_args o Input.source_explode; val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; diff -r 24e2b098bf44 -r d09d71223e7a src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Mar 29 20:53:52 2016 +0200 +++ b/src/Pure/pure_thy.ML Tue Mar 29 21:17:29 2016 +0200 @@ -22,18 +22,24 @@ val qualify = Binding.qualify true Context.PureN; +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); +fun delimfix sy = Delimfix (Input.string sy, Position.no_range); +fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range); +fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range); +fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range); + (* application syntax variants *) val appl_syntax = - [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)), - ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]; + [("_appl", typ "('b => 'a) => args => logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)), + ("_appl", typ "('b => 'a) => args => aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]; val applC_syntax = - [("", typ "'a => cargs", Delimfix "_"), - ("_cargs", typ "'a => cargs => cargs", Mixfix ("_/ _", [1000, 1000], 1000)), - ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)), - ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))]; + [("", typ "'a => cargs", delimfix "_"), + ("_cargs", typ "'a => cargs => cargs", mixfix ("_/ _", [1000, 1000], 1000)), + ("_applC", typ "('b => 'a) => cargs => logic", mixfix ("(1_/ _)", [1000, 1000], 999)), + ("_applC", typ "('b => 'a) => cargs => aprop", mixfix ("(1_/ _)", [1000, 1000], 999))]; structure Old_Appl_Syntax = Theory_Data ( @@ -81,120 +87,120 @@ "class_name"])) #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) #> Sign.add_syntax Syntax.mode_default - [("", typ "prop' => prop", Delimfix "_"), - ("", typ "logic => any", Delimfix "_"), - ("", typ "prop' => any", Delimfix "_"), - ("", typ "logic => logic", Delimfix "'(_')"), - ("", typ "prop' => prop'", Delimfix "'(_')"), - ("_constrain", typ "logic => type => logic", Mixfix ("_::_", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_::_", [4, 0], 3)), + [("", typ "prop' => prop", delimfix "_"), + ("", typ "logic => any", delimfix "_"), + ("", typ "prop' => any", delimfix "_"), + ("", typ "logic => logic", delimfix "'(_')"), + ("", typ "prop' => prop'", delimfix "'(_')"), + ("_constrain", typ "logic => type => logic", mixfix ("_::_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", mixfix ("_::_", [4, 0], 3)), ("_ignore_type", typ "'a", NoSyn), - ("", typ "tid_position => type", Delimfix "_"), - ("", typ "tvar_position => type", Delimfix "_"), - ("", typ "type_name => type", Delimfix "_"), - ("_type_name", typ "id => type_name", Delimfix "_"), - ("_type_name", typ "longid => type_name", Delimfix "_"), - ("_ofsort", typ "tid_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)), - ("_ofsort", typ "tvar_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)), - ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], 1000)), - ("", typ "class_name => sort", Delimfix "_"), - ("_class_name", typ "id => class_name", Delimfix "_"), - ("_class_name", typ "longid => class_name", Delimfix "_"), - ("_topsort", typ "sort", Delimfix "{}"), - ("_sort", typ "classes => sort", Delimfix "{_}"), - ("", typ "class_name => classes", Delimfix "_"), - ("_classes", typ "class_name => classes => classes", Delimfix "_,_"), - ("_tapp", typ "type => type_name => type", Mixfix ("_ _", [1000, 0], 1000)), - ("_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)), - ("", typ "type => type", Delimfix "'(_')"), - ("\<^type>dummy", typ "type", Delimfix "'_"), + ("", typ "tid_position => type", delimfix "_"), + ("", typ "tvar_position => type", delimfix "_"), + ("", typ "type_name => type", delimfix "_"), + ("_type_name", typ "id => type_name", delimfix "_"), + ("_type_name", typ "longid => type_name", delimfix "_"), + ("_ofsort", typ "tid_position => sort => type", mixfix ("_::_", [1000, 0], 1000)), + ("_ofsort", typ "tvar_position => sort => type", mixfix ("_::_", [1000, 0], 1000)), + ("_dummy_ofsort", typ "sort => type", mixfix ("'_()::_", [0], 1000)), + ("", typ "class_name => sort", delimfix "_"), + ("_class_name", typ "id => class_name", delimfix "_"), + ("_class_name", typ "longid => class_name", delimfix "_"), + ("_topsort", typ "sort", delimfix "{}"), + ("_sort", typ "classes => sort", delimfix "{_}"), + ("", typ "class_name => classes", delimfix "_"), + ("_classes", typ "class_name => classes => classes", delimfix "_,_"), + ("_tapp", typ "type => type_name => type", mixfix ("_ _", [1000, 0], 1000)), + ("_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)), + ("", 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 "_,/ _"), - ("", typ "id_position => idt", Delimfix "_"), - ("_idtdummy", typ "idt", Delimfix "'_"), - ("_idtyp", typ "id_position => type => idt", Mixfix ("_::_", [], 0)), - ("_idtypdummy", typ "type => idt", Mixfix ("'_()::_", [], 0)), - ("", typ "idt => idt", Delimfix "'(_')"), - ("", typ "idt => idts", Delimfix "_"), - ("_idts", typ "idt => idts => idts", Mixfix ("_/ _", [1, 0], 0)), - ("", typ "idt => pttrn", Delimfix "_"), - ("", typ "pttrn => pttrns", Delimfix "_"), - ("_pttrns", typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)), - ("", typ "aprop => aprop", Delimfix "'(_')"), - ("", typ "id_position => aprop", Delimfix "_"), - ("", typ "longid_position => aprop", Delimfix "_"), - ("", typ "var_position => 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 ("((1\_\)/ \ _)", [0, 1], 1)), - ("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"), + ("", typ "'a => args", delimfix "_"), + ("_args", typ "'a => args => args", delimfix "_,/ _"), + ("", typ "id_position => idt", delimfix "_"), + ("_idtdummy", typ "idt", delimfix "'_"), + ("_idtyp", typ "id_position => type => idt", mixfix ("_::_", [], 0)), + ("_idtypdummy", typ "type => idt", mixfix ("'_()::_", [], 0)), + ("", typ "idt => idt", delimfix "'(_')"), + ("", typ "idt => idts", delimfix "_"), + ("_idts", typ "idt => idts => idts", mixfix ("_/ _", [1, 0], 0)), + ("", typ "idt => pttrn", delimfix "_"), + ("", typ "pttrn => pttrns", delimfix "_"), + ("_pttrns", typ "pttrn => pttrns => pttrns", mixfix ("_/ _", [1, 0], 0)), + ("", typ "aprop => aprop", delimfix "'(_')"), + ("", typ "id_position => aprop", delimfix "_"), + ("", typ "longid_position => aprop", delimfix "_"), + ("", typ "var_position => 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 ("((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 "\"), + ("_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 "\"), ("_strip_positions", typ "'a", NoSyn), - ("_position", typ "num_token => num_position", Delimfix "_"), - ("_position", typ "float_token => float_position", Delimfix "_"), - ("_constify", typ "num_position => num_const", Delimfix "_"), - ("_constify", typ "float_position => float_const", Delimfix "_"), - ("_index", typ "logic => index", Delimfix "(00\<^bsub>_\<^esub>)"), - ("_indexdefault", typ "index", Delimfix ""), - ("_indexvar", typ "index", Delimfix "'\"), + ("_position", typ "num_token => num_position", delimfix "_"), + ("_position", typ "float_token => float_position", delimfix "_"), + ("_constify", typ "num_position => num_const", delimfix "_"), + ("_constify", typ "float_position => float_const", delimfix "_"), + ("_index", typ "logic => index", delimfix "(00\<^bsub>_\<^esub>)"), + ("_indexdefault", typ "index", delimfix ""), + ("_indexvar", typ "index", delimfix "'\"), ("_struct", typ "index => logic", NoSyn), ("_update_name", typ "idt", NoSyn), ("_constrainAbs", typ "'a", NoSyn), - ("_position_sort", typ "tid => tid_position", Delimfix "_"), - ("_position_sort", typ "tvar => tvar_position", Delimfix "_"), - ("_position", typ "id => id_position", Delimfix "_"), - ("_position", typ "longid => longid_position", Delimfix "_"), - ("_position", typ "var => var_position", Delimfix "_"), - ("_position", typ "str_token => str_position", Delimfix "_"), - ("_position", typ "string_token => string_position", Delimfix "_"), - ("_position", typ "cartouche => cartouche_position", Delimfix "_"), + ("_position_sort", typ "tid => tid_position", delimfix "_"), + ("_position_sort", typ "tvar => tvar_position", delimfix "_"), + ("_position", typ "id => id_position", delimfix "_"), + ("_position", typ "longid => longid_position", delimfix "_"), + ("_position", typ "var => var_position", delimfix "_"), + ("_position", typ "str_token => str_position", delimfix "_"), + ("_position", typ "string_token => string_position", delimfix "_"), + ("_position", typ "cartouche => cartouche_position", delimfix "_"), ("_type_constraint_", typ "'a", NoSyn), - ("_context_const", typ "id_position => logic", Delimfix "CONST _"), - ("_context_const", typ "id_position => aprop", Delimfix "CONST _"), - ("_context_const", typ "longid_position => logic", Delimfix "CONST _"), - ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"), - ("_context_xconst", typ "id_position => logic", Delimfix "XCONST _"), - ("_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.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))] + ("_context_const", typ "id_position => logic", delimfix "CONST _"), + ("_context_const", typ "id_position => aprop", delimfix "CONST _"), + ("_context_const", typ "longid_position => logic", delimfix "CONST _"), + ("_context_const", typ "longid_position => aprop", delimfix "CONST _"), + ("_context_xconst", typ "id_position => logic", delimfix "XCONST _"), + ("_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.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 (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 "...")] + [(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))] + [(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))] #> Sign.add_consts - [(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 ("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 "'_")] + (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", delimfix "'_")] #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) [] #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) [] #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []