more position information for type mixfix;
authorwenzelm
Tue Mar 29 21:17:29 2016 +0200 (2016-03-29)
changeset 62752d09d71223e7a
parent 62751 24e2b098bf44
child 62753 76b814ccce61
more position information for type mixfix;
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/Pure/General/input.ML
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/parse.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Syntax/local_syntax.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 29 20:53:52 2016 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 29 21:17:29 2016 +0200
     1.3 @@ -87,29 +87,31 @@
     1.4  
     1.5  type atom_pool = ((string * int) * int list) list
     1.6  
     1.7 +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range)
     1.8 +
     1.9  fun add_wacky_syntax ctxt =
    1.10    let
    1.11      val name_of = fst o dest_Const
    1.12      val thy = Proof_Context.theory_of ctxt
    1.13      val (unrep_s, thy) = thy
    1.14        |> Sign.declare_const_global ((@{binding nitpick_unrep}, @{typ 'a}),
    1.15 -        Mixfix (unrep_mixfix (), [], 1000))
    1.16 +        mixfix (unrep_mixfix (), [], 1000))
    1.17        |>> name_of
    1.18      val (maybe_s, thy) = thy
    1.19        |> Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    1.20 -        Mixfix (maybe_mixfix (), [1000], 1000))
    1.21 +        mixfix (maybe_mixfix (), [1000], 1000))
    1.22        |>> name_of
    1.23      val (abs_s, thy) = thy
    1.24        |> Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
    1.25 -        Mixfix (abs_mixfix (), [40], 40))
    1.26 +        mixfix (abs_mixfix (), [40], 40))
    1.27        |>> name_of
    1.28      val (base_s, thy) = thy
    1.29        |> Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}),
    1.30 -        Mixfix (base_mixfix (), [1000], 1000))
    1.31 +        mixfix (base_mixfix (), [1000], 1000))
    1.32        |>> name_of
    1.33      val (step_s, thy) = thy
    1.34        |> Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
    1.35 -        Mixfix (step_mixfix (), [1000], 1000))
    1.36 +        mixfix (step_mixfix (), [1000], 1000))
    1.37        |>> name_of
    1.38    in
    1.39      (((unrep_s, maybe_s, abs_s), (base_s, step_s)),
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Mar 29 20:53:52 2016 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Mar 29 21:17:29 2016 +0200
     2.3 @@ -1959,8 +1959,8 @@
     2.4      val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
     2.5      val setT = HOLogic.mk_setT T
     2.6      val elems = HOLogic.mk_set T ts
     2.7 -    val ([dots], ctxt') =
     2.8 -      Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt
     2.9 +    val ([dots], ctxt') = ctxt
    2.10 +      |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Delimfix (\<open>...\<close>, Position.no_range))]
    2.11      (* check expected values *)
    2.12      val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
    2.13      val () =
     3.1 --- a/src/Pure/General/input.ML	Tue Mar 29 20:53:52 2016 +0200
     3.2 +++ b/src/Pure/General/input.ML	Tue Mar 29 21:17:29 2016 +0200
     3.3 @@ -15,6 +15,7 @@
     3.4    val string: string -> source
     3.5    val source_explode: source -> Symbol_Pos.T list
     3.6    val source_content: source -> string
     3.7 +  val equal_content: source * source -> bool
     3.8  end;
     3.9  
    3.10  structure Input: INPUT =
    3.11 @@ -38,6 +39,8 @@
    3.12  
    3.13  val source_content = source_explode #> Symbol_Pos.content;
    3.14  
    3.15 +val equal_content = (op =) o apply2 source_content;
    3.16 +
    3.17  end;
    3.18  
    3.19  end;
     4.1 --- a/src/Pure/Isar/class.ML	Tue Mar 29 20:53:52 2016 +0200
     4.2 +++ b/src/Pure/Isar/class.ML	Tue Mar 29 21:17:29 2016 +0200
     4.3 @@ -616,8 +616,10 @@
     4.4  fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
     4.5    (case instantiation_param lthy b of
     4.6      SOME c =>
     4.7 -      if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
     4.8 -      else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
     4.9 +      if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
    4.10 +      else
    4.11 +        error ("Illegal mixfix syntax for overloaded constant " ^ quote c ^
    4.12 +          Position.here (Mixfix.pos_of mx))
    4.13    | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
    4.14  
    4.15  fun pretty lthy =
     5.1 --- a/src/Pure/Isar/expression.ML	Tue Mar 29 20:53:52 2016 +0200
     5.2 +++ b/src/Pure/Isar/expression.ML	Tue Mar 29 21:17:29 2016 +0200
     5.3 @@ -85,8 +85,11 @@
     5.4          [] => ()
     5.5        | dups => error (message ^ commas dups));
     5.6  
     5.7 -    fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso
     5.8 -      (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
     5.9 +    fun parm_eq ((p1, mx1), (p2, mx2)) =
    5.10 +      p1 = p2 andalso
    5.11 +        (Mixfix.equal (mx1, mx2) orelse
    5.12 +          error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^
    5.13 +            Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2]));
    5.14  
    5.15      fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
    5.16      fun params_inst (loc, (prfx, Positional insts)) =
     6.1 --- a/src/Pure/Isar/generic_target.ML	Tue Mar 29 20:53:52 2016 +0200
     6.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Mar 29 21:17:29 2016 +0200
     6.3 @@ -103,14 +103,17 @@
     6.4        warning
     6.5          ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
     6.6            commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
     6.7 -          (if mx = NoSyn then ""
     6.8 -           else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
     6.9 +          (if Mixfix.is_empty mx then ""
    6.10 +           else
    6.11 +            "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx) ^
    6.12 +              Position.here (Mixfix.pos_of mx)))
    6.13      else (); NoSyn);
    6.14  
    6.15  fun check_mixfix_global (b, no_params) mx =
    6.16 -  if no_params orelse mx = NoSyn then mx
    6.17 -  else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
    6.18 -    Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
    6.19 +  if no_params orelse Mixfix.is_empty mx then mx
    6.20 +  else
    6.21 +    (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
    6.22 +      Pretty.string_of (Mixfix.pretty_mixfix mx) ^ Position.here (Mixfix.pos_of mx)); NoSyn);
    6.23  
    6.24  fun same_const (Const (c, _), Const (c', _)) = c = c'
    6.25    | same_const (t $ _, t' $ _) = same_const (t, t')
     7.1 --- a/src/Pure/Isar/overloading.ML	Tue Mar 29 20:53:52 2016 +0200
     7.2 +++ b/src/Pure/Isar/overloading.ML	Tue Mar 29 21:17:29 2016 +0200
     7.3 @@ -158,9 +158,11 @@
     7.4  fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
     7.5    (case operation lthy b of
     7.6      SOME (c, (v, checked)) =>
     7.7 -      if mx <> NoSyn
     7.8 -      then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
     7.9 -      else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
    7.10 +      if Mixfix.is_empty mx then
    7.11 +        lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
    7.12 +      else
    7.13 +        error ("Illegal mixfix syntax for overloaded constant " ^ quote c ^
    7.14 +          Position.here (Mixfix.pos_of mx))
    7.15    | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
    7.16  
    7.17  fun pretty lthy =
     8.1 --- a/src/Pure/Isar/parse.ML	Tue Mar 29 20:53:52 2016 +0200
     8.2 +++ b/src/Pure/Isar/parse.ML	Tue Mar 29 21:17:29 2016 +0200
     8.3 @@ -317,22 +317,33 @@
     8.4  
     8.5  local
     8.6  
     8.7 -val mfix = string --
     8.8 -  !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
     8.9 -    Scan.optional nat 1000) >> (Mixfix o Scan.triple2);
    8.10 +val mfix =
    8.11 +  input string --
    8.12 +    !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000)
    8.13 +  >> (fn (sy, (ps, p)) => Mixfix (sy, ps, p, Position.no_range));
    8.14 +
    8.15 +val infx =
    8.16 +  $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => Infix (sy, p, Position.no_range)));
    8.17  
    8.18 -val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
    8.19 -val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
    8.20 -val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
    8.21 -val strcture = $$$ "structure" >> K Structure;
    8.22 +val infxl =
    8.23 +  $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => Infixl (sy, p, Position.no_range)));
    8.24 +
    8.25 +val infxr =
    8.26 +  $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => Infixr (sy, p, Position.no_range)));
    8.27  
    8.28 -val binder = $$$ "binder" |--
    8.29 -  !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
    8.30 -  >> (Binder o Scan.triple2);
    8.31 +val strcture = $$$ "structure" >> K (Structure Position.no_range);
    8.32 +
    8.33 +val binder =
    8.34 +  $$$ "binder" |--
    8.35 +    !!! (input string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
    8.36 +  >> (fn (sy, (p, q)) => Binder (sy, p, q, Position.no_range));
    8.37  
    8.38  val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
    8.39  
    8.40 -fun annotation guard body = $$$ "(" |-- guard (body --| $$$ ")");
    8.41 +fun annotation guard body =
    8.42 +  Scan.trace ($$$ "(" |-- guard (body --| $$$ ")"))
    8.43 +    >> (fn (mx, toks) => Mixfix.set_range (Token.range_of toks) mx);
    8.44 +
    8.45  fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn;
    8.46  
    8.47  in
     9.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Mar 29 20:53:52 2016 +0200
     9.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Mar 29 21:17:29 2016 +0200
     9.3 @@ -30,6 +30,7 @@
     9.4  val idtT = Type ("idt", []);
     9.5  val aT = TFree (Name.aT, []);
     9.6  
     9.7 +
     9.8  (** constants for theorems and axioms **)
     9.9  
    9.10  fun add_proof_atom_consts names thy =
    9.11 @@ -37,8 +38,12 @@
    9.12    |> Sign.root_path
    9.13    |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
    9.14  
    9.15 +
    9.16  (** constants for application and abstraction **)
    9.17  
    9.18 +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
    9.19 +fun delimfix sy = Delimfix (Input.string sy, Position.no_range);
    9.20 +
    9.21  fun add_proof_syntax thy =
    9.22    thy
    9.23    |> Sign.root_path
    9.24 @@ -46,29 +51,29 @@
    9.25    |> Sign.add_types_global
    9.26      [(Binding.make ("proof", @{here}), 0, NoSyn)]
    9.27    |> fold (snd oo Sign.declare_const_global)
    9.28 -    [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
    9.29 -     ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
    9.30 +    [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
    9.31 +     ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
    9.32       ((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn),
    9.33       ((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn),
    9.34       ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
    9.35       ((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn),
    9.36       ((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn),
    9.37 -     ((Binding.make ("MinProof", @{here}), proofT), Delimfix "?")]
    9.38 +     ((Binding.make ("MinProof", @{here}), proofT), delimfix "?")]
    9.39    |> Sign.add_nonterminals_global
    9.40      [Binding.make ("param", @{here}),
    9.41       Binding.make ("params", @{here})]
    9.42    |> Sign.add_syntax Syntax.mode_default
    9.43 -    [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
    9.44 -     ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    9.45 -     ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    9.46 -     ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
    9.47 -     ("", paramT --> paramT, Delimfix "'(_')"),
    9.48 -     ("", idtT --> paramsT, Delimfix "_"),
    9.49 -     ("", paramT --> paramsT, Delimfix "_")]
    9.50 +    [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
    9.51 +     ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
    9.52 +     ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
    9.53 +     ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)),
    9.54 +     ("", paramT --> paramT, delimfix "'(_')"),
    9.55 +     ("", idtT --> paramsT, delimfix "_"),
    9.56 +     ("", paramT --> paramsT, delimfix "_")]
    9.57    |> Sign.add_syntax (Print_Mode.ASCII, true)
    9.58 -    [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    9.59 -     (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    9.60 -     (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4))]
    9.61 +    [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)),
    9.62 +     (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
    9.63 +     (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
    9.64    |> Sign.add_trrules (map Syntax.Parse_Print_Rule
    9.65      [(Ast.mk_appl (Ast.Constant "_Lam")
    9.66          [Ast.mk_appl (Ast.Constant "_Lam0")
    10.1 --- a/src/Pure/Syntax/local_syntax.ML	Tue Mar 29 20:53:52 2016 +0200
    10.2 +++ b/src/Pure/Syntax/local_syntax.ML	Tue Mar 29 21:17:29 2016 +0200
    10.3 @@ -76,20 +76,21 @@
    10.4  
    10.5  local
    10.6  
    10.7 -fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
    10.8 +fun prep_mixfix _ _ (_, (_, _, Structure _)) = NONE
    10.9    | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
   10.10    | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
   10.11    | prep_mixfix add mode (Fixed, (x, T, mx)) =
   10.12        SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx)));
   10.13  
   10.14 -fun prep_struct (Fixed, (c, _, Structure)) = SOME c
   10.15 -  | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
   10.16 +fun prep_struct (Fixed, (c, _, Structure _)) = SOME c
   10.17 +  | prep_struct (_, (c, _, mx as Structure _)) =
   10.18 +      error ("Bad mixfix declaration for " ^ quote c ^ Position.here (Mixfix.pos_of mx))
   10.19    | prep_struct _ = NONE;
   10.20  
   10.21  in
   10.22  
   10.23  fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) =
   10.24 -  (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
   10.25 +  (case filter_out (Mixfix.is_empty o #3 o #2) raw_decls of
   10.26      [] => (NONE, syntax)
   10.27    | decls =>
   10.28        let
    11.1 --- a/src/Pure/Syntax/mixfix.ML	Tue Mar 29 20:53:52 2016 +0200
    11.2 +++ b/src/Pure/Syntax/mixfix.ML	Tue Mar 29 21:17:29 2016 +0200
    11.3 @@ -8,18 +8,23 @@
    11.4  sig
    11.5    datatype mixfix =
    11.6      NoSyn |
    11.7 -    Mixfix of string * int list * int |
    11.8 -    Delimfix of string |
    11.9 -    Infix of string * int |
   11.10 -    Infixl of string * int |
   11.11 -    Infixr of string * int |
   11.12 -    Binder of string * int * int |
   11.13 -    Structure
   11.14 +    Mixfix of Input.source * int list * int * Position.range |
   11.15 +    Delimfix of Input.source * Position.range |
   11.16 +    Infix of Input.source * int * Position.range |
   11.17 +    Infixl of Input.source * int * Position.range |
   11.18 +    Infixr of Input.source * int * Position.range |
   11.19 +    Binder of Input.source * int * int * Position.range |
   11.20 +    Structure of Position.range
   11.21  end;
   11.22  
   11.23  signature MIXFIX =
   11.24  sig
   11.25    include BASIC_MIXFIX
   11.26 +  val is_empty: mixfix -> bool
   11.27 +  val equal: mixfix * mixfix -> bool
   11.28 +  val set_range: Position.range -> mixfix -> mixfix
   11.29 +  val range_of: mixfix -> Position.range
   11.30 +  val pos_of: mixfix -> Position.T
   11.31    val pretty_mixfix: mixfix -> Pretty.T
   11.32    val mixfix_args: mixfix -> int
   11.33    val mixfixT: mixfix -> typ
   11.34 @@ -36,20 +41,57 @@
   11.35  
   11.36  datatype mixfix =
   11.37    NoSyn |
   11.38 -  Mixfix of string * int list * int |
   11.39 -  Delimfix of string |
   11.40 -  Infix of string * int |
   11.41 -  Infixl of string * int |
   11.42 -  Infixr of string * int |
   11.43 -  Binder of string * int * int |
   11.44 -  Structure;
   11.45 +  Mixfix of Input.source * int list * int * Position.range |
   11.46 +  Delimfix of Input.source * Position.range |
   11.47 +  Infix of Input.source * int * Position.range |
   11.48 +  Infixl of Input.source * int * Position.range |
   11.49 +  Infixr of Input.source * int * Position.range |
   11.50 +  Binder of Input.source * int * int * Position.range |
   11.51 +  Structure of Position.range;
   11.52 +
   11.53 +fun is_empty NoSyn = true
   11.54 +  | is_empty _ = false;
   11.55 +
   11.56 +fun equal (NoSyn, NoSyn) = true
   11.57 +  | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) =
   11.58 +      Input.equal_content (sy, sy') andalso ps = ps' andalso p = p'
   11.59 +  | equal (Delimfix (sy, _), Delimfix (sy', _)) = Input.equal_content (sy, sy')
   11.60 +  | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
   11.61 +  | equal (Infixl (sy, p, _), Infixl (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
   11.62 +  | equal (Infixr (sy, p, _), Infixr (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
   11.63 +  | equal (Binder (sy, p, q, _), Binder (sy', p', q', _)) =
   11.64 +      Input.equal_content (sy, sy') andalso p = p' andalso q = q'
   11.65 +  | equal (Structure _, Structure _) = true
   11.66 +  | equal _ = false;
   11.67 +
   11.68 +fun set_range range mx =
   11.69 +  (case mx of
   11.70 +    NoSyn => NoSyn
   11.71 +  | Mixfix (sy, ps, p, _) => Mixfix (sy, ps, p, range)
   11.72 +  | Delimfix (sy, _) => Delimfix (sy, range)
   11.73 +  | Infix (sy, p, _) => Infix (sy, p, range)
   11.74 +  | Infixl (sy, p, _) => Infixl (sy, p, range)
   11.75 +  | Infixr (sy, p, _) => Infixr (sy, p, range)
   11.76 +  | Binder (sy, p, q, _) => Binder (sy, p, q, range)
   11.77 +  | Structure _ => Structure range);
   11.78 +
   11.79 +fun range_of NoSyn = Position.no_range
   11.80 +  | range_of (Mixfix (_, _, _, range)) = range
   11.81 +  | range_of (Delimfix (_, range)) = range
   11.82 +  | range_of (Infix (_, _, range)) = range
   11.83 +  | range_of (Infixl (_, _, range)) = range
   11.84 +  | range_of (Infixr (_, _, range)) = range
   11.85 +  | range_of (Binder (_, _, _, range)) = range
   11.86 +  | range_of (Structure range) = range;
   11.87 +
   11.88 +val pos_of = Position.set_range o range_of;
   11.89  
   11.90  
   11.91  (* pretty_mixfix *)
   11.92  
   11.93  local
   11.94  
   11.95 -val quoted = Pretty.quote o Pretty.str;
   11.96 +val quoted = Pretty.quote o Pretty.str o Input.source_content;
   11.97  val keyword = Pretty.keyword2;
   11.98  val parens = Pretty.enclose "(" ")";
   11.99  val brackets = Pretty.enclose "[" "]";
  11.100 @@ -58,15 +100,15 @@
  11.101  in
  11.102  
  11.103  fun pretty_mixfix NoSyn = Pretty.str ""
  11.104 -  | pretty_mixfix (Mixfix (s, ps, p)) =
  11.105 +  | pretty_mixfix (Mixfix (s, ps, p, _)) =
  11.106        parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
  11.107 -  | pretty_mixfix (Delimfix s) = parens [quoted s]
  11.108 -  | pretty_mixfix (Infix (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
  11.109 -  | pretty_mixfix (Infixl (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
  11.110 -  | pretty_mixfix (Infixr (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
  11.111 -  | pretty_mixfix (Binder (s, p1, p2)) =
  11.112 +  | pretty_mixfix (Delimfix (s, _)) = parens [quoted s]
  11.113 +  | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
  11.114 +  | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
  11.115 +  | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
  11.116 +  | pretty_mixfix (Binder (s, p1, p2, _)) =
  11.117        parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
  11.118 -  | pretty_mixfix Structure = parens [keyword "structure"];
  11.119 +  | pretty_mixfix (Structure _) = parens [keyword "structure"];
  11.120  
  11.121  end;
  11.122  
  11.123 @@ -74,13 +116,13 @@
  11.124  (* syntax specifications *)
  11.125  
  11.126  fun mixfix_args NoSyn = 0
  11.127 -  | mixfix_args (Mixfix (sy, _, _)) = Syntax_Ext.mfix_args sy
  11.128 -  | mixfix_args (Delimfix sy) = Syntax_Ext.mfix_args sy
  11.129 -  | mixfix_args (Infix (sy, _)) = 2 + Syntax_Ext.mfix_args sy
  11.130 -  | mixfix_args (Infixl (sy, _)) = 2 + Syntax_Ext.mfix_args sy
  11.131 -  | mixfix_args (Infixr (sy, _)) = 2 + Syntax_Ext.mfix_args sy
  11.132 +  | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy
  11.133 +  | mixfix_args (Delimfix (sy, _)) = Syntax_Ext.mixfix_args sy
  11.134 +  | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
  11.135 +  | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
  11.136 +  | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
  11.137    | mixfix_args (Binder _) = 1
  11.138 -  | mixfix_args Structure = 0;
  11.139 +  | mixfix_args (Structure _) = 0;
  11.140  
  11.141  fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
  11.142    | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
  11.143 @@ -93,19 +135,26 @@
  11.144  
  11.145  fun syn_ext_types type_decls =
  11.146    let
  11.147 -    fun mk_infix sy ty t p1 p2 p3 = Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
  11.148 +    fun mk_infix sy ty t p1 p2 p3 =
  11.149 +      Syntax_Ext.Mfix
  11.150 +        (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
  11.151 +          ty, t, [p1, p2], p3);
  11.152  
  11.153      fun mfix_of (_, _, NoSyn) = NONE
  11.154 -      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
  11.155 -      | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], 1000))
  11.156 -      | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
  11.157 -      | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
  11.158 -      | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
  11.159 +      | mfix_of (t, ty, Mixfix (sy, ps, p, _)) =
  11.160 +          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p))
  11.161 +      | mfix_of (t, ty, Delimfix (sy, _)) =
  11.162 +          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000))
  11.163 +      | mfix_of (t, ty, Infix (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
  11.164 +      | mfix_of (t, ty, Infixl (sy, p, _)) = SOME (mk_infix sy ty t p (p + 1) p)
  11.165 +      | mfix_of (t, ty, Infixr (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) p p)
  11.166        | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);
  11.167  
  11.168 -    fun check_args (_, ty, _) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) =
  11.169 +    fun check_args (_, ty, mx) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) =
  11.170            if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
  11.171 -          else Syntax_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
  11.172 +          else
  11.173 +            error ("Bad number of type constructor arguments in mixfix annotation" ^
  11.174 +              Position.here (pos_of mx))
  11.175        | check_args _ NONE = ();
  11.176  
  11.177      val mfix = map mfix_of type_decls;
  11.178 @@ -122,22 +171,30 @@
  11.179  fun syn_ext_consts logical_types const_decls =
  11.180    let
  11.181      fun mk_infix sy ty c p1 p2 p3 =
  11.182 -      [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
  11.183 -       Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
  11.184 +      [Syntax_Ext.Mfix
  11.185 +        (Symbol_Pos.explode0 "op " @ Input.source_explode sy, ty, c, [], 1000),
  11.186 +       Syntax_Ext.Mfix
  11.187 +        (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
  11.188 +          ty, c, [p1, p2], p3)];
  11.189  
  11.190      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
  11.191            [Type ("idts", []), ty2] ---> ty3
  11.192        | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
  11.193  
  11.194      fun mfix_of (_, _, NoSyn) = []
  11.195 -      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
  11.196 -      | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], 1000)]
  11.197 -      | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
  11.198 -      | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
  11.199 -      | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
  11.200 -      | mfix_of (c, ty, Binder (sy, p, q)) =
  11.201 -          [Syntax_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
  11.202 -      | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);
  11.203 +      | mfix_of (c, ty, Mixfix (sy, ps, p, _)) =
  11.204 +          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p)]
  11.205 +      | mfix_of (c, ty, Delimfix (sy, _)) =
  11.206 +          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000)]
  11.207 +      | mfix_of (c, ty, Infix (sy, p, _)) = mk_infix sy ty c (p + 1) (p + 1) p
  11.208 +      | mfix_of (c, ty, Infixl (sy, p, _)) = mk_infix sy ty c p (p + 1) p
  11.209 +      | mfix_of (c, ty, Infixr (sy, p, _)) = mk_infix sy ty c (p + 1) p p
  11.210 +      | mfix_of (c, ty, Binder (sy, p, q, _)) =
  11.211 +          [Syntax_Ext.Mfix
  11.212 +            (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)",
  11.213 +              binder_typ c ty, (binder_name c), [0, p], q)]
  11.214 +      | mfix_of (c, _, mx) =
  11.215 +          error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx));
  11.216  
  11.217      fun binder (c, _, Binder _) = SOME (binder_name c, c)
  11.218        | binder _ = NONE;
  11.219 @@ -159,4 +216,3 @@
  11.220  
  11.221  structure Basic_Mixfix: BASIC_MIXFIX = Mixfix;
  11.222  open Basic_Mixfix;
  11.223 -
    12.1 --- a/src/Pure/Syntax/syntax.ML	Tue Mar 29 20:53:52 2016 +0200
    12.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Mar 29 21:17:29 2016 +0200
    12.3 @@ -602,9 +602,9 @@
    12.4  fun guess_infix (Syntax ({gram, ...}, _)) c =
    12.5    (case Parser.guess_infix_lr (Lazy.force gram) c of
    12.6      SOME (s, l, r, j) => SOME
    12.7 -     (if l then Mixfix.Infixl (s, j)
    12.8 -      else if r then Mixfix.Infixr (s, j)
    12.9 -      else Mixfix.Infix (s, j))
   12.10 +     (if l then Mixfix.Infixl (Input.string s, j, Position.no_range)
   12.11 +      else if r then Mixfix.Infixr (Input.string s, j, Position.no_range)
   12.12 +      else Mixfix.Infix (Input.string s, j, Position.no_range))
   12.13    | NONE => NONE);
   12.14  
   12.15  
    13.1 --- a/src/Pure/Syntax/syntax_ext.ML	Tue Mar 29 20:53:52 2016 +0200
    13.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Tue Mar 29 21:17:29 2016 +0200
    13.3 @@ -7,8 +7,7 @@
    13.4  signature SYNTAX_EXT =
    13.5  sig
    13.6    val dddot_indexname: indexname
    13.7 -  datatype mfix = Mfix of string * typ * string * int list * int
    13.8 -  val err_in_mfix: string -> mfix -> 'a
    13.9 +  datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int
   13.10    val typ_to_nonterm: typ -> string
   13.11    datatype xsymb =
   13.12      Delim of string |
   13.13 @@ -28,8 +27,8 @@
   13.14        print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
   13.15        print_rules: (Ast.ast * Ast.ast) list,
   13.16        print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}
   13.17 -  val mfix_delims: string -> string list
   13.18 -  val mfix_args: string -> int
   13.19 +  val mfix_args: Symbol_Pos.T list -> int
   13.20 +  val mixfix_args: Input.source -> int
   13.21    val escape: string -> string
   13.22    val syn_ext': string list -> mfix list ->
   13.23      (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   13.24 @@ -112,16 +111,16 @@
   13.25  (** datatype mfix **)
   13.26  
   13.27  (*Mfix (sy, ty, c, ps, p):
   13.28 -    sy: rhs of production as symbolic string
   13.29 +    sy: rhs of production as symbolic text
   13.30      ty: type description of production
   13.31      c: head of parse tree
   13.32      ps: priorities of arguments in sy
   13.33      p: priority of production*)
   13.34  
   13.35 -datatype mfix = Mfix of string * typ * string * int list * int;
   13.36 +datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int;
   13.37  
   13.38  fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
   13.39 -  cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
   13.40 +  cat_error msg ("in mixfix annotation " ^ quote (Symbol_Pos.content sy) ^ " for " ^ quote const);
   13.41  
   13.42  
   13.43  (* typ_to_nonterm *)
   13.44 @@ -140,11 +139,17 @@
   13.45  
   13.46  local
   13.47  
   13.48 +open Basic_Symbol_Pos;
   13.49 +
   13.50 +fun scan_one pred = Scan.one (pred o Symbol_Pos.symbol);
   13.51 +fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol);
   13.52 +fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol);
   13.53 +
   13.54  val is_meta = member (op =) ["(", ")", "/", "_", "\<index>"];
   13.55  
   13.56  val scan_delim_char =
   13.57 -  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
   13.58 -  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
   13.59 +  $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
   13.60 +  scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
   13.61  
   13.62  fun read_int ["0", "0"] = ~1
   13.63    | read_int cs = #1 (Library.read_int cs);
   13.64 @@ -152,19 +157,19 @@
   13.65  val scan_sym =
   13.66    $$ "_" >> K (Argument ("", 0)) ||
   13.67    $$ "\<index>" >> K index ||
   13.68 -  $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
   13.69 +  $$ "(" |-- scan_many Symbol.is_digit >> (Bg o read_int o map Symbol_Pos.symbol) ||
   13.70    $$ ")" >> K En ||
   13.71    $$ "/" -- $$ "/" >> K (Brk ~1) ||
   13.72 -  $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
   13.73 -  Scan.many1 Symbol.is_blank >> (Space o implode) ||
   13.74 -  Scan.repeat1 scan_delim_char >> (Delim o implode);
   13.75 +  $$ "/" |-- scan_many Symbol.is_blank >> (Brk o length) ||
   13.76 +  scan_many1 Symbol.is_blank >> (Space o Symbol_Pos.content) ||
   13.77 +  Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
   13.78  
   13.79  val scan_symb =
   13.80    scan_sym >> SOME ||
   13.81 -  $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
   13.82 +  $$ "'" -- scan_one Symbol.is_blank >> K NONE;
   13.83  
   13.84  val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
   13.85 -val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
   13.86 +val read_symbs = map_filter I o the o Scan.read Symbol_Pos.stopper scan_symbs;
   13.87  
   13.88  fun unique_index xsymbs =
   13.89    if length (filter is_index xsymbs) <= 1 then xsymbs
   13.90 @@ -172,10 +177,10 @@
   13.91  
   13.92  in
   13.93  
   13.94 -val read_mfix = unique_index o read_symbs o Symbol.explode;
   13.95 +val read_mfix = unique_index o read_symbs;
   13.96  
   13.97 -fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
   13.98  val mfix_args = length o filter is_argument o read_mfix;
   13.99 +val mixfix_args = mfix_args o Input.source_explode;
  13.100  
  13.101  val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
  13.102  
    14.1 --- a/src/Pure/pure_thy.ML	Tue Mar 29 20:53:52 2016 +0200
    14.2 +++ b/src/Pure/pure_thy.ML	Tue Mar 29 21:17:29 2016 +0200
    14.3 @@ -22,18 +22,24 @@
    14.4  
    14.5  val qualify = Binding.qualify true Context.PureN;
    14.6  
    14.7 +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
    14.8 +fun delimfix sy = Delimfix (Input.string sy, Position.no_range);
    14.9 +fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range);
   14.10 +fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
   14.11 +fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
   14.12 +
   14.13  
   14.14  (* application syntax variants *)
   14.15  
   14.16  val appl_syntax =
   14.17 - [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
   14.18 -  ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
   14.19 + [("_appl", typ "('b => 'a) => args => logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
   14.20 +  ("_appl", typ "('b => 'a) => args => aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
   14.21  
   14.22  val applC_syntax =
   14.23 - [("",       typ "'a => cargs",                  Delimfix "_"),
   14.24 -  ("_cargs", typ "'a => cargs => cargs",         Mixfix ("_/ _", [1000, 1000], 1000)),
   14.25 -  ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
   14.26 -  ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
   14.27 + [("",       typ "'a => cargs",                  delimfix "_"),
   14.28 +  ("_cargs", typ "'a => cargs => cargs",         mixfix ("_/ _", [1000, 1000], 1000)),
   14.29 +  ("_applC", typ "('b => 'a) => cargs => logic", mixfix ("(1_/ _)", [1000, 1000], 999)),
   14.30 +  ("_applC", typ "('b => 'a) => cargs => aprop", mixfix ("(1_/ _)", [1000, 1000], 999))];
   14.31  
   14.32  structure Old_Appl_Syntax = Theory_Data
   14.33  (
   14.34 @@ -81,120 +87,120 @@
   14.35          "class_name"]))
   14.36    #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
   14.37    #> Sign.add_syntax Syntax.mode_default
   14.38 -   [("",            typ "prop' => prop",               Delimfix "_"),
   14.39 -    ("",            typ "logic => any",                Delimfix "_"),
   14.40 -    ("",            typ "prop' => any",                Delimfix "_"),
   14.41 -    ("",            typ "logic => logic",              Delimfix "'(_')"),
   14.42 -    ("",            typ "prop' => prop'",              Delimfix "'(_')"),
   14.43 -    ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
   14.44 -    ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
   14.45 +   [("",            typ "prop' => prop",               delimfix "_"),
   14.46 +    ("",            typ "logic => any",                delimfix "_"),
   14.47 +    ("",            typ "prop' => any",                delimfix "_"),
   14.48 +    ("",            typ "logic => logic",              delimfix "'(_')"),
   14.49 +    ("",            typ "prop' => prop'",              delimfix "'(_')"),
   14.50 +    ("_constrain",  typ "logic => type => logic",      mixfix ("_::_", [4, 0], 3)),
   14.51 +    ("_constrain",  typ "prop' => type => prop'",      mixfix ("_::_", [4, 0], 3)),
   14.52      ("_ignore_type", typ "'a",                         NoSyn),
   14.53 -    ("",            typ "tid_position => type",        Delimfix "_"),
   14.54 -    ("",            typ "tvar_position => type",       Delimfix "_"),
   14.55 -    ("",            typ "type_name => type",           Delimfix "_"),
   14.56 -    ("_type_name",  typ "id => type_name",             Delimfix "_"),
   14.57 -    ("_type_name",  typ "longid => type_name",         Delimfix "_"),
   14.58 -    ("_ofsort",     typ "tid_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
   14.59 -    ("_ofsort",     typ "tvar_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
   14.60 -    ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], 1000)),
   14.61 -    ("",            typ "class_name => sort",          Delimfix "_"),
   14.62 -    ("_class_name", typ "id => class_name",            Delimfix "_"),
   14.63 -    ("_class_name", typ "longid => class_name",        Delimfix "_"),
   14.64 -    ("_topsort",    typ "sort",                        Delimfix "{}"),
   14.65 -    ("_sort",       typ "classes => sort",             Delimfix "{_}"),
   14.66 -    ("",            typ "class_name => classes",       Delimfix "_"),
   14.67 -    ("_classes",    typ "class_name => classes => classes", Delimfix "_,_"),
   14.68 -    ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [1000, 0], 1000)),
   14.69 -    ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
   14.70 -    ("",            typ "type => types",               Delimfix "_"),
   14.71 -    ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
   14.72 -    ("\<^type>fun", typ "type => type => type",        Mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
   14.73 -    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
   14.74 -    ("",            typ "type => type",                Delimfix "'(_')"),
   14.75 -    ("\<^type>dummy", typ "type",                      Delimfix "'_"),
   14.76 +    ("",            typ "tid_position => type",        delimfix "_"),
   14.77 +    ("",            typ "tvar_position => type",       delimfix "_"),
   14.78 +    ("",            typ "type_name => type",           delimfix "_"),
   14.79 +    ("_type_name",  typ "id => type_name",             delimfix "_"),
   14.80 +    ("_type_name",  typ "longid => type_name",         delimfix "_"),
   14.81 +    ("_ofsort",     typ "tid_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
   14.82 +    ("_ofsort",     typ "tvar_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
   14.83 +    ("_dummy_ofsort", typ "sort => type",              mixfix ("'_()::_", [0], 1000)),
   14.84 +    ("",            typ "class_name => sort",          delimfix "_"),
   14.85 +    ("_class_name", typ "id => class_name",            delimfix "_"),
   14.86 +    ("_class_name", typ "longid => class_name",        delimfix "_"),
   14.87 +    ("_topsort",    typ "sort",                        delimfix "{}"),
   14.88 +    ("_sort",       typ "classes => sort",             delimfix "{_}"),
   14.89 +    ("",            typ "class_name => classes",       delimfix "_"),
   14.90 +    ("_classes",    typ "class_name => classes => classes", delimfix "_,_"),
   14.91 +    ("_tapp",       typ "type => type_name => type",   mixfix ("_ _", [1000, 0], 1000)),
   14.92 +    ("_tappl",      typ "type => types => type_name => type", delimfix "((1'(_,/ _')) _)"),
   14.93 +    ("",            typ "type => types",               delimfix "_"),
   14.94 +    ("_types",      typ "type => types => types",      delimfix "_,/ _"),
   14.95 +    ("\<^type>fun", typ "type => type => type",        mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
   14.96 +    ("_bracket",    typ "types => type => type",       mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
   14.97 +    ("",            typ "type => type",                delimfix "'(_')"),
   14.98 +    ("\<^type>dummy", typ "type",                      delimfix "'_"),
   14.99      ("_type_prop",  typ "'a",                          NoSyn),
  14.100 -    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
  14.101 +    ("_lambda",     typ "pttrns => 'a => logic",       mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
  14.102      ("_abs",        typ "'a",                          NoSyn),
  14.103 -    ("",            typ "'a => args",                  Delimfix "_"),
  14.104 -    ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
  14.105 -    ("",            typ "id_position => idt",          Delimfix "_"),
  14.106 -    ("_idtdummy",   typ "idt",                         Delimfix "'_"),
  14.107 -    ("_idtyp",      typ "id_position => type => idt",  Mixfix ("_::_", [], 0)),
  14.108 -    ("_idtypdummy", typ "type => idt",                 Mixfix ("'_()::_", [], 0)),
  14.109 -    ("",            typ "idt => idt",                  Delimfix "'(_')"),
  14.110 -    ("",            typ "idt => idts",                 Delimfix "_"),
  14.111 -    ("_idts",       typ "idt => idts => idts",         Mixfix ("_/ _", [1, 0], 0)),
  14.112 -    ("",            typ "idt => pttrn",                Delimfix "_"),
  14.113 -    ("",            typ "pttrn => pttrns",             Delimfix "_"),
  14.114 -    ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
  14.115 -    ("",            typ "aprop => aprop",              Delimfix "'(_')"),
  14.116 -    ("",            typ "id_position => aprop",        Delimfix "_"),
  14.117 -    ("",            typ "longid_position => aprop",    Delimfix "_"),
  14.118 -    ("",            typ "var_position => aprop",       Delimfix "_"),
  14.119 -    ("_DDDOT",      typ "aprop",                       Delimfix "\<dots>"),
  14.120 -    ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
  14.121 -    ("_asm",        typ "prop => asms",                Delimfix "_"),
  14.122 -    ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
  14.123 -    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
  14.124 -    ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
  14.125 +    ("",            typ "'a => args",                  delimfix "_"),
  14.126 +    ("_args",       typ "'a => args => args",          delimfix "_,/ _"),
  14.127 +    ("",            typ "id_position => idt",          delimfix "_"),
  14.128 +    ("_idtdummy",   typ "idt",                         delimfix "'_"),
  14.129 +    ("_idtyp",      typ "id_position => type => idt",  mixfix ("_::_", [], 0)),
  14.130 +    ("_idtypdummy", typ "type => idt",                 mixfix ("'_()::_", [], 0)),
  14.131 +    ("",            typ "idt => idt",                  delimfix "'(_')"),
  14.132 +    ("",            typ "idt => idts",                 delimfix "_"),
  14.133 +    ("_idts",       typ "idt => idts => idts",         mixfix ("_/ _", [1, 0], 0)),
  14.134 +    ("",            typ "idt => pttrn",                delimfix "_"),
  14.135 +    ("",            typ "pttrn => pttrns",             delimfix "_"),
  14.136 +    ("_pttrns",     typ "pttrn => pttrns => pttrns",   mixfix ("_/ _", [1, 0], 0)),
  14.137 +    ("",            typ "aprop => aprop",              delimfix "'(_')"),
  14.138 +    ("",            typ "id_position => aprop",        delimfix "_"),
  14.139 +    ("",            typ "longid_position => aprop",    delimfix "_"),
  14.140 +    ("",            typ "var_position => aprop",       delimfix "_"),
  14.141 +    ("_DDDOT",      typ "aprop",                       delimfix "\<dots>"),
  14.142 +    ("_aprop",      typ "aprop => prop",               delimfix "PROP _"),
  14.143 +    ("_asm",        typ "prop => asms",                delimfix "_"),
  14.144 +    ("_asms",       typ "prop => asms => asms",        delimfix "_;/ _"),
  14.145 +    ("_bigimpl",    typ "asms => prop => prop",        mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
  14.146 +    ("_ofclass",    typ "type => logic => prop",       delimfix "(1OFCLASS/(1'(_,/ _')))"),
  14.147      ("_mk_ofclass", typ "dummy",                       NoSyn),
  14.148 -    ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
  14.149 -    ("",            typ "id_position => logic",        Delimfix "_"),
  14.150 -    ("",            typ "longid_position => logic",    Delimfix "_"),
  14.151 -    ("",            typ "var_position => logic",       Delimfix "_"),
  14.152 -    ("_DDDOT",      typ "logic",                       Delimfix "\<dots>"),
  14.153 +    ("_TYPE",       typ "type => logic",               delimfix "(1TYPE/(1'(_')))"),
  14.154 +    ("",            typ "id_position => logic",        delimfix "_"),
  14.155 +    ("",            typ "longid_position => logic",    delimfix "_"),
  14.156 +    ("",            typ "var_position => logic",       delimfix "_"),
  14.157 +    ("_DDDOT",      typ "logic",                       delimfix "\<dots>"),
  14.158      ("_strip_positions", typ "'a", NoSyn),
  14.159 -    ("_position",   typ "num_token => num_position",   Delimfix "_"),
  14.160 -    ("_position",   typ "float_token => float_position", Delimfix "_"),
  14.161 -    ("_constify",   typ "num_position => num_const",   Delimfix "_"),
  14.162 -    ("_constify",   typ "float_position => float_const", Delimfix "_"),
  14.163 -    ("_index",      typ "logic => index",              Delimfix "(00\<^bsub>_\<^esub>)"),
  14.164 -    ("_indexdefault", typ "index",                     Delimfix ""),
  14.165 -    ("_indexvar",   typ "index",                       Delimfix "'\<index>"),
  14.166 +    ("_position",   typ "num_token => num_position",   delimfix "_"),
  14.167 +    ("_position",   typ "float_token => float_position", delimfix "_"),
  14.168 +    ("_constify",   typ "num_position => num_const",   delimfix "_"),
  14.169 +    ("_constify",   typ "float_position => float_const", delimfix "_"),
  14.170 +    ("_index",      typ "logic => index",              delimfix "(00\<^bsub>_\<^esub>)"),
  14.171 +    ("_indexdefault", typ "index",                     delimfix ""),
  14.172 +    ("_indexvar",   typ "index",                       delimfix "'\<index>"),
  14.173      ("_struct",     typ "index => logic",              NoSyn),
  14.174      ("_update_name", typ "idt",                        NoSyn),
  14.175      ("_constrainAbs", typ "'a",                        NoSyn),
  14.176 -    ("_position_sort", typ "tid => tid_position",      Delimfix "_"),
  14.177 -    ("_position_sort", typ "tvar => tvar_position",    Delimfix "_"),
  14.178 -    ("_position",   typ "id => id_position",           Delimfix "_"),
  14.179 -    ("_position",   typ "longid => longid_position",   Delimfix "_"),
  14.180 -    ("_position",   typ "var => var_position",         Delimfix "_"),
  14.181 -    ("_position",   typ "str_token => str_position",   Delimfix "_"),
  14.182 -    ("_position",   typ "string_token => string_position", Delimfix "_"),
  14.183 -    ("_position",   typ "cartouche => cartouche_position", Delimfix "_"),
  14.184 +    ("_position_sort", typ "tid => tid_position",      delimfix "_"),
  14.185 +    ("_position_sort", typ "tvar => tvar_position",    delimfix "_"),
  14.186 +    ("_position",   typ "id => id_position",           delimfix "_"),
  14.187 +    ("_position",   typ "longid => longid_position",   delimfix "_"),
  14.188 +    ("_position",   typ "var => var_position",         delimfix "_"),
  14.189 +    ("_position",   typ "str_token => str_position",   delimfix "_"),
  14.190 +    ("_position",   typ "string_token => string_position", delimfix "_"),
  14.191 +    ("_position",   typ "cartouche => cartouche_position", delimfix "_"),
  14.192      ("_type_constraint_", typ "'a",                    NoSyn),
  14.193 -    ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
  14.194 -    ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
  14.195 -    ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
  14.196 -    ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
  14.197 -    ("_context_xconst", typ "id_position => logic",    Delimfix "XCONST _"),
  14.198 -    ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
  14.199 -    ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
  14.200 -    ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
  14.201 -    (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
  14.202 -    ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
  14.203 -    (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
  14.204 -    (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
  14.205 +    ("_context_const", typ "id_position => logic",     delimfix "CONST _"),
  14.206 +    ("_context_const", typ "id_position => aprop",     delimfix "CONST _"),
  14.207 +    ("_context_const", typ "longid_position => logic", delimfix "CONST _"),
  14.208 +    ("_context_const", typ "longid_position => aprop", delimfix "CONST _"),
  14.209 +    ("_context_xconst", typ "id_position => logic",    delimfix "XCONST _"),
  14.210 +    ("_context_xconst", typ "id_position => aprop",    delimfix "XCONST _"),
  14.211 +    ("_context_xconst", typ "longid_position => logic", delimfix "XCONST _"),
  14.212 +    ("_context_xconst", typ "longid_position => aprop", delimfix "XCONST _"),
  14.213 +    (const "Pure.dummy_pattern", typ "aprop",          delimfix "'_"),
  14.214 +    ("_sort_constraint", typ "type => prop",           delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
  14.215 +    (const "Pure.term", typ "logic => prop",           delimfix "TERM _"),
  14.216 +    (const "Pure.conjunction", typ "prop => prop => prop", infixr_ ("&&&", 2))]
  14.217    #> Sign.add_syntax Syntax.mode_default applC_syntax
  14.218    #> Sign.add_syntax (Print_Mode.ASCII, true)
  14.219 -   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ => _)", [1, 0], 0)),
  14.220 -    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ => _)", [0, 0], 0)),
  14.221 -    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3%_./ _)", [0, 3], 3)),
  14.222 -    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("==", 2)),
  14.223 -    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3!!_./ _)", [0, 0], 0)),
  14.224 -    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("==>", 1)),
  14.225 -    ("_DDDOT",            typ "aprop",                  Delimfix "..."),
  14.226 -    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
  14.227 -    ("_DDDOT",            typ "logic",                  Delimfix "...")]
  14.228 +   [(tycon "fun",         typ "type => type => type",   mixfix ("(_/ => _)", [1, 0], 0)),
  14.229 +    ("_bracket",          typ "types => type => type",  mixfix ("([_]/ => _)", [0, 0], 0)),
  14.230 +    ("_lambda",           typ "pttrns => 'a => logic",  mixfix ("(3%_./ _)", [0, 3], 3)),
  14.231 +    (const "Pure.eq",     typ "'a => 'a => prop",       infix_ ("==", 2)),
  14.232 +    (const "Pure.all_binder", typ "idts => prop => prop", mixfix ("(3!!_./ _)", [0, 0], 0)),
  14.233 +    (const "Pure.imp",    typ "prop => prop => prop",   infixr_ ("==>", 1)),
  14.234 +    ("_DDDOT",            typ "aprop",                  delimfix "..."),
  14.235 +    ("_bigimpl",          typ "asms => prop => prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
  14.236 +    ("_DDDOT",            typ "logic",                  delimfix "...")]
  14.237    #> Sign.add_syntax ("", false)
  14.238 -   [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
  14.239 +   [(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))]
  14.240    #> Sign.add_consts
  14.241 -   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\<equiv>", 2)),
  14.242 -    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\<Longrightarrow>", 1)),
  14.243 -    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\<And>", 0, 0)),
  14.244 +   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", infix_ ("\<equiv>", 2)),
  14.245 +    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", infixr_ ("\<Longrightarrow>", 1)),
  14.246 +    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", binder ("\<And>", 0, 0)),
  14.247      (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
  14.248      (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
  14.249 -    (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
  14.250 +    (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", delimfix "'_")]
  14.251    #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
  14.252    #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
  14.253    #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []