# HG changeset patch
# User wenzelm
# Date 1459374432 -7200
# Node ID 42a997773bb0b3529228cba06e1c0a6b792097e8
# Parent  d4b7d128ec5ad166557228eb6c204878fb3e42e6# Parent  b486f512a471aaf44c05699affd0ab636ad5ccdb
merged

diff -r d4b7d128ec5a -r 42a997773bb0 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Mar 30 15:16:50 2016 +0200
+++ b/Admin/components/components.sha1	Wed Mar 30 23:47:12 2016 +0200
@@ -92,6 +92,7 @@
 14ce124c897abfa23713928dc034d6ef0e1c5031  jedit_build-20150228.tar.gz
 b5f7115384c167559211768eb5fe98138864473b  jedit_build-20151023.tar.gz
 8ba7b6791be788f316427cdcd805daeaa6935190  jedit_build-20151124.tar.gz
+c70c5a6c565d435a09a8639f8afd3de360708e1c  jedit_build-20160330.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 c8a19a36adf6cefa779d85f22ded2f4654e68ea5  jortho-1.0-1.tar.gz
diff -r d4b7d128ec5a -r 42a997773bb0 Admin/components/main
--- a/Admin/components/main	Wed Mar 30 15:16:50 2016 +0200
+++ b/Admin/components/main	Wed Mar 30 23:47:12 2016 +0200
@@ -6,7 +6,7 @@
 Haskabelle-2015
 isabelle_fonts-20160227
 jdk-8u72
-jedit_build-20151124
+jedit_build-20160330
 jfreechart-1.0.14-1
 jortho-1.0-2
 kodkodi-1.5.2
diff -r d4b7d128ec5a -r 42a997773bb0 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -78,10 +78,13 @@
     (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
   end
 
-fun prepare_function do_print prep default_constraint fixspec eqns config lthy =
+fun prepare_function do_print prep fixspec eqns config lthy =
   let
-    val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
-    val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
+    val ((fixes0, spec0), ctxt') =
+      lthy
+      |> Proof_Context.set_object_logic_constraint
+      |> prep fixspec eqns
+      ||> Proof_Context.restore_object_logic_constraint lthy;
     val fixes = map (apfst (apfst Binding.name_of)) fixes0;
     val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
@@ -143,10 +146,10 @@
     ((goal_state, afterqed), lthy')
   end
 
-fun gen_add_function do_print prep default_constraint fixspec eqns config tac lthy =
+fun gen_add_function do_print prep fixspec eqns config tac lthy =
   let
     val ((goal_state, afterqed), lthy') =
-      prepare_function do_print prep default_constraint fixspec eqns config lthy
+      prepare_function do_print prep fixspec eqns config lthy
     val pattern_thm =
       case SINGLE (tac lthy') goal_state of
         NONE => error "pattern completeness and compatibility proof failed"
@@ -156,28 +159,21 @@
     |> afterqed [[pattern_thm]]
   end
 
-val default_constraint_any = Type_Infer.anyT @{sort type};
-val default_constraint_any' = YXML.string_of_body (Term_XML.Encode.typ default_constraint_any);
+val add_function = gen_add_function false Specification.check_spec
+fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec a b c d
 
-val add_function =
-  gen_add_function false Specification.check_spec default_constraint_any
-fun add_function_cmd a b c d int =
-  gen_add_function int Specification.read_spec default_constraint_any' a b c d
-
-fun gen_function do_print prep default_constraint fixspec eqns config lthy =
+fun gen_function do_print prep fixspec eqns config lthy =
   let
     val ((goal_state, afterqed), lthy') =
-      prepare_function do_print prep default_constraint fixspec eqns config lthy
+      prepare_function do_print prep fixspec eqns config lthy
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
     |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
   end
 
-val function =
-  gen_function false Specification.check_spec default_constraint_any
-fun function_cmd a b c int =
-  gen_function int Specification.read_spec default_constraint_any' a b c
+val function = gen_function false Specification.check_spec
+fun function_cmd a b c int = gen_function int Specification.read_spec a b c
 
 fun prepare_termination_proof prep_term raw_term_opt lthy =
   let
diff -r d4b7d128ec5a -r 42a997773bb0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -1960,7 +1960,7 @@
     val setT = HOLogic.mk_setT T
     val elems = HOLogic.mk_set T ts
     val ([dots], ctxt') = ctxt
-      |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Delimfix (\<open>...\<close>, Position.no_range))]
+      |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix.mixfix "...")]
     (* check expected values *)
     val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
     val () =
diff -r d4b7d128ec5a -r 42a997773bb0 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -134,7 +134,11 @@
     val (opt_var, ctxt) =
       (case raw_var of
         NONE => (NONE, lthy)
-      | SOME var => prep_var var lthy |>> SOME)
+      | SOME var =>
+          Proof_Context.set_object_logic_constraint lthy
+          |> prep_var var
+          ||> Proof_Context.restore_object_logic_constraint lthy
+          |>> SOME)
     val lhs_constraint = (case opt_var of SOME (_, SOME T, _) => T | _ => dummyT)
 
     fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt;
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/General/input.ML
--- a/src/Pure/General/input.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/General/input.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -13,6 +13,7 @@
   val range_of: source -> Position.range
   val source: bool -> Symbol_Pos.text -> Position.range -> source
   val string: string -> source
+  val reset_pos: source -> source
   val source_explode: source -> Symbol_Pos.T list
   val source_content: source -> string
   val equal_content: source * source -> bool
@@ -24,6 +25,9 @@
 abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}
 with
 
+
+(* source *)
+
 fun is_delimited (Source {delimited, ...}) = delimited;
 fun text_of (Source {text, ...}) = text;
 fun pos_of (Source {range = (pos, _), ...}) = pos;
@@ -34,6 +38,11 @@
 
 fun string text = source true text Position.no_range;
 
+fun reset_pos (Source {delimited, text, ...}) = source delimited text Position.no_range;
+
+
+(* content *)
+
 fun source_explode (Source {text, range = (pos, _), ...}) =
   Symbol_Pos.explode (text, pos);
 
@@ -44,4 +53,3 @@
 end;
 
 end;
-
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -12,6 +12,7 @@
   val assmsN: string
   val abs_params: term -> term -> term
   val goal: Proof.context -> term list -> (indexname * term option) list
+  val dddot: indexname
   val facts: Proof.context -> term list -> (indexname * term option) list
   val no_facts: indexname list
 end;
@@ -40,6 +41,15 @@
   | goal _ _ = [((thesisN, 0), NONE)];
 
 
+(* dddot *)
+
+val dddot = ("dddot", 0);
+
+val _ =
+  Theory.setup (Sign.parse_translation
+    [("_DDDOT", fn _ => fn ts => Term.list_comb (Syntax.var dddot, ts))]);
+
+
 (* facts *)
 
 fun get_arg ctxt prop =
@@ -50,9 +60,8 @@
 fun facts ctxt props =
   (case try List.last props of
     NONE => []
-  | SOME prop =>
-      [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
+  | SOME prop => [(dddot, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
 
-val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)];
+val no_facts = [dddot, (thisN, 0)];
 
 end;
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Isar/class.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -617,9 +617,7 @@
   (case instantiation_param lthy b of
     SOME c =>
       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))
+      else error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
   | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -10,6 +10,7 @@
   (*auxiliary*)
   val export_abbrev: Proof.context ->
       (term -> term) -> term -> term * ((string * sort) list * (term list * term list))
+  val check_mixfix: Proof.context -> binding * (string * sort) list -> mixfix -> mixfix
   val check_mixfix_global: binding * bool -> mixfix -> mixfix
 
   (*background primitives*)
@@ -104,16 +105,14 @@
         ("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 Mixfix.is_empty mx then ""
-           else
-            "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx) ^
-              Position.here (Mixfix.pos_of mx)))
+           else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
     else (); NoSyn);
 
 fun check_mixfix_global (b, no_params) mx =
   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);
+      Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
 
 fun same_const (Const (c, _), Const (c', _)) = c = c'
   | same_const (t $ _, t' $ _) = same_const (t, t')
@@ -148,10 +147,12 @@
           |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)])
       | NONE =>
           context
-          |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
+          |> Proof_Context.generic_add_abbrev Print_Mode.internal
+            (b', Term.close_schematic_term rhs')
           |-> (fn (const as Const (c, _), _) => same_stem ?
                 (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
-                 same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
+                 same_shape ?
+                  Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
     end
   else context;
 
@@ -347,8 +348,10 @@
     (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
       (fn (lhs, _) =>  (* FIXME type_params!? *)
         Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs))
-  #-> (fn lhs => standard_const (op <>) prmode
-          ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
+  #-> (fn lhs =>
+        standard_const (op <>) prmode
+          ((b, if null (snd params) then NoSyn else mx),
+            Term.list_comb (Logic.unvarify_global lhs, snd params)));
 
 
 (** theory operations **)
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -160,9 +160,7 @@
     SOME (c, (v, checked)) =>
       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))
+      else error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
   | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -320,29 +320,29 @@
 val mfix =
   input string --
     !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000)
-  >> (fn (sy, (ps, p)) => Mixfix (sy, ps, p, Position.no_range));
+  >> (fn (sy, (ps, p)) => fn range => Mixfix (sy, ps, p, range));
 
 val infx =
-  $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => Infix (sy, p, Position.no_range)));
+  $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infix (sy, p, range)));
 
 val infxl =
-  $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => Infixl (sy, p, Position.no_range)));
+  $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infixl (sy, p, range)));
 
 val infxr =
-  $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => Infixr (sy, p, Position.no_range)));
+  $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infixr (sy, p, range)));
 
-val strcture = $$$ "structure" >> K (Structure Position.no_range);
+val strcture = $$$ "structure" >> K Structure;
 
 val binder =
   $$$ "binder" |--
     !!! (input string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
-  >> (fn (sy, (p, q)) => Binder (sy, p, q, Position.no_range));
+  >> (fn (sy, (p, q)) => fn range => Binder (sy, p, q, range));
 
 val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
 
 fun annotation guard body =
   Scan.trace ($$$ "(" |-- guard (body --| $$$ ")"))
-    >> (fn (mx, toks) => Mixfix.set_range (Token.range_of toks) mx);
+    >> (fn (mx, toks) => mx (Token.range_of toks));
 
 fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn;
 
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -594,21 +594,25 @@
 
 local
 
+fun read_arg (c, mx) ctxt =
+  (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
+    Free (x, _) =>
+      let
+        val ctxt' =
+          ctxt |> is_none (Variable.default_type ctxt x) ?
+            Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx));
+        val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
+      in ((t, mx), ctxt') end
+  | t => ((t, mx), ctxt));
+
 fun gen_write prep_arg mode args =
   assert_forward
-  #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
+  #> map_context (fold_map prep_arg args #-> Proof_Context.notation true mode)
   #> reset_facts;
 
-fun read_arg ctxt (c, mx) =
-  (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
-    Free (x, _) =>
-      let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
-      in (Free (x, T), mx) end
-  | t => (t, mx));
-
 in
 
-val write = gen_write (K I);
+val write = gen_write pair;
 val write_cmd = gen_write read_arg;
 
 end;
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -130,6 +130,9 @@
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
+  val set_object_logic_constraint: Proof.context -> Proof.context
+  val restore_object_logic_constraint: Proof.context -> Proof.context -> Proof.context
+  val default_constraint: Proof.context -> mixfix -> typ
   val read_var: binding * string option * mixfix -> Proof.context ->
     (binding * typ option * mixfix) * Proof.context
   val cert_var: binding * typ option * mixfix -> Proof.context ->
@@ -1056,11 +1059,37 @@
 
 (** basic logical entities **)
 
+(* default type constraint *)
+
+val object_logic_constraint =
+  Config.bool
+    (Config.declare ("Proof_Context.object_logic_constraint", @{here}) (K (Config.Bool false)));
+
+val set_object_logic_constraint = Config.put object_logic_constraint true;
+fun restore_object_logic_constraint ctxt =
+  Config.put object_logic_constraint (Config.get ctxt object_logic_constraint);
+
+fun default_constraint ctxt mx =
+  let
+    val A =
+      (case (Object_Logic.get_base_sort ctxt, Config.get ctxt object_logic_constraint) of
+        (SOME S, true) => Type_Infer.anyT S
+      | _ => dummyT);
+  in
+    (case mx of
+      Binder _ => (A --> A) --> A
+    | _ => replicate (Mixfix.mixfix_args mx) A ---> A)
+  end;
+
+
 (* variables *)
 
 fun declare_var (x, opt_T, mx) ctxt =
-  let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx)
-  in ((x, T, mx), ctxt |> Variable.declare_constraints (Free (x, T))) end;
+  let val T = (case opt_T of SOME T => T | NONE => default_constraint ctxt mx)
+  in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
+
+fun add_syntax vars ctxt =
+  map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt;
 
 fun check_var internal b =
   let
@@ -1073,6 +1102,13 @@
 
 local
 
+fun check_mixfix ctxt (b, T, mx) =
+  let
+    val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt;
+    val mx' = Mixfix.reset_pos mx;
+    val _ = add_syntax [(x, T, if Context_Position.is_visible ctxt then mx else mx')] ctxt';
+  in mx' end;
+
 fun prep_var prep_typ internal (b, raw_T, mx) ctxt =
   let
     val x = check_var internal b;
@@ -1080,8 +1116,9 @@
       if internal then T
       else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
     val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
-    val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
-  in ((b, opt_T, mx), ctxt') end;
+    val (T, ctxt') = ctxt |> declare_var (x, opt_T, mx);
+    val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt' (b, T, mx);
+  in ((b, SOME T, mx'), ctxt') end;
 
 in
 
@@ -1182,12 +1219,10 @@
   let
     val (vars, _) = fold_map prep_var raw_vars ctxt;
     val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
-  in
-    ctxt'
-    |> fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
-    |-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
-    |> pair xs
-  end;
+    val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars;
+    val (Ts, ctxt'') = fold_map declare_var vars' ctxt';
+    val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars';
+  in (xs, add_syntax vars'' ctxt'') end;
 
 in
 
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -232,7 +232,7 @@
       fst (prep (the_list raw_var) [raw_spec] lthy);
     val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
     val _ = Name.reject_internal (x, []);
-    val var as (b, _) =
+    val (b, mx) =
       (case vars of
         [] => (Binding.make (x, get_pos x), NoSyn)
       | [((b, _), mx)] =>
@@ -244,7 +244,7 @@
           in (b, mx) end);
     val name = Binding.reset_pos (Thm.def_binding_optional b raw_name);
     val ((lhs, (_, raw_th)), lthy2) = lthy
-      |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));
+      |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
     val th = prove lthy2 raw_th;
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
@@ -275,7 +275,7 @@
         (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
     val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
     val _ = Name.reject_internal (x, []);
-    val var =
+    val (b, mx) =
       (case vars of
         [] => (Binding.make (x, get_pos x), NoSyn)
       | [((b, _), mx)] =>
@@ -286,7 +286,7 @@
                 Position.here (Binding.pos_of b));
           in (b, mx) end);
     val lthy2 = lthy1
-      |> Local_Theory.abbrev mode (var, rhs) |> snd
+      |> Local_Theory.abbrev mode ((b, mx), rhs) |> snd
       |> Proof_Context.restore_syntax_mode lthy;
 
     val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -43,6 +43,7 @@
   val language_verbatim: bool -> T
   val language_rail: T
   val language_path: T
+  val language_mixfix: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val get_entity_kind: T -> string option
@@ -317,9 +318,11 @@
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
-val language_verbatim = language' {name = "verbatim", symbols = true, antiquotes = false};
+val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
 val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
+val language_mixfix =
+  language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
 
 
 (* formal entities *)
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -42,7 +42,6 @@
 (** 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
@@ -58,7 +57,7 @@
      ((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), Mixfix.mixfix "?")]
   |> Sign.add_nonterminals_global
     [Binding.make ("param", @{here}),
      Binding.make ("params", @{here})]
@@ -67,9 +66,9 @@
      ("_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 "_")]
+     ("", paramT --> paramT, Mixfix.mixfix "'(_')"),
+     ("", idtT --> paramsT, Mixfix.mixfix "_"),
+     ("", paramT --> paramsT, Mixfix.mixfix "_")]
   |> 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)),
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -83,8 +83,7 @@
       SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx)));
 
 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 (_, (c, _, Structure _)) = error ("Bad structure mixfix declaration for " ^ quote c)
   | prep_struct _ = NONE;
 
 in
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -9,7 +9,6 @@
   datatype mixfix =
     NoSyn |
     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 |
@@ -20,14 +19,14 @@
 signature MIXFIX =
 sig
   include BASIC_MIXFIX
+  val mixfix: string -> 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 reset_pos: mixfix -> mixfix
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
-  val mixfixT: mixfix -> typ
   val make_type: int -> typ
   val binder_name: string -> string
   val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
@@ -42,20 +41,20 @@
 datatype mixfix =
   NoSyn |
   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 mixfix s = Mixfix (Input.string s, [], 1000, Position.no_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'
@@ -64,20 +63,8 @@
   | 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
@@ -86,6 +73,14 @@
 
 val pos_of = Position.set_range o range_of;
 
+fun reset_pos NoSyn = NoSyn
+  | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)
+  | reset_pos (Infix (sy, p, _)) = Infix (Input.reset_pos sy, p, Position.no_range)
+  | reset_pos (Infixl (sy, p, _)) = Infixl (Input.reset_pos sy, p, Position.no_range)
+  | reset_pos (Infixr (sy, p, _)) = Infixr (Input.reset_pos sy, p, Position.no_range)
+  | reset_pos (Binder (sy, p, q, _)) = Binder (Input.reset_pos sy, p, q, Position.no_range)
+  | reset_pos (Structure _) = Structure Position.no_range;
+
 
 (* pretty_mixfix *)
 
@@ -102,7 +97,6 @@
 fun pretty_mixfix NoSyn = Pretty.str ""
   | 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])
@@ -117,16 +111,12 @@
 
 fun mixfix_args NoSyn = 0
   | 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;
 
-fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
-  | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
-
 
 (* syn_ext_types *)
 
@@ -143,8 +133,6 @@
     fun mfix_of (_, _, NoSyn) = NONE
       | mfix_of (t, ty, Mixfix (sy, ps, p, range)) =
           SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range))
-      | mfix_of (t, ty, Delimfix (sy, range)) =
-          SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000, Position.set_range range))
       | mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range)
       | mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range)
       | mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range)
@@ -172,8 +160,8 @@
   let
     fun mk_infix sy ty c p1 p2 p3 range =
       [Syntax_Ext.Mfix
-        (Symbol_Pos.explode0 "op " @ Input.source_explode sy,
-          ty, c, [], 1000, Position.set_range range),
+        (Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy),
+          ty, c, [], 1000, Position.none),
        Syntax_Ext.Mfix
         (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
           ty, c, [p1, p2], p3, Position.set_range range)];
@@ -185,8 +173,6 @@
     fun mfix_of (_, _, NoSyn) = []
       | mfix_of (c, ty, Mixfix (sy, ps, p, range)) =
           [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)]
-      | mfix_of (c, ty, Delimfix (sy, range)) =
-          [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000, Position.set_range range)]
       | mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range
       | mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range
       | mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -6,7 +6,6 @@
 
 signature SYNTAX_EXT =
 sig
-  val dddot_indexname: indexname
   datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
   val typ_to_nonterm: typ -> string
   datatype xsymb =
@@ -56,12 +55,6 @@
 structure Syntax_Ext: SYNTAX_EXT =
 struct
 
-
-(** misc definitions **)
-
-val dddot_indexname = ("dddot", 0);
-
-
 (** datatype xprod **)
 
 (*Delim s: delimiter s
@@ -106,6 +99,14 @@
     fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
   |> map Symbol.explode;
 
+fun reports_of (xsym, pos: Position.T) =
+  (case xsym of
+    Delim _ => [(pos, Markup.literal)]
+  | Bg _ => [(pos, Markup.keyword3)]
+  | Brk _ => [(pos, Markup.keyword3)]
+  | En => [(pos, Markup.keyword3)]
+  | _ => []);
+
 
 
 (** datatype mfix **)
@@ -163,21 +164,21 @@
   Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
 
 val scan_symb =
-  scan_sym >> SOME ||
+  Scan.trace scan_sym >>
+    (fn (syms, trace) => SOME (syms, Position.set_range (Symbol_Pos.range trace))) ||
   $$ "'" -- 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_Pos.stopper scan_symbs;
-
-fun unique_index xsymbs =
-  if length (filter is_index xsymbs) <= 1 then xsymbs
-  else error "Duplicate index arguments (\<index>)";
 
 in
 
-val read_mfix = unique_index o read_symbs;
+fun read_mfix ss =
+  let
+    val xsymbs = map_filter I (the (Scan.read Symbol_Pos.stopper scan_symbs ss));
+    val _ = Position.reports (maps reports_of xsymbs);
+  in xsymbs end;
 
-val mfix_args = length o filter is_argument o read_mfix;
+val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none));
 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;
@@ -189,90 +190,93 @@
 
 fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
   let
-    val is_logtype = member (op =) logical_types;
-
-    fun err msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
+    val _ = Position.report pos Markup.language_mixfix;
+    val symbs0 = read_mfix sy;
 
-    fun check_pri p =
-      if p >= 0 andalso p <= 1000 then ()
-      else err ("Precedence " ^ string_of_int p ^ " out of range");
+    fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
 
-    fun blocks_ok [] 0 = true
-      | blocks_ok [] _ = false
-      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
-      | blocks_ok (En :: _) 0 = false
-      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
-      | blocks_ok (_ :: syms) n = blocks_ok syms n;
-
-    fun check_blocks syms =
-      if blocks_ok syms 0 then ()
-      else err "Unbalanced block parentheses";
-
-
-    val cons_fst = apfst o cons;
+    fun check_blocks [] pending bad = pending @ bad
+      | check_blocks ((Bg _, pos) :: rest) pending bad = check_blocks rest (pos :: pending) bad
+      | check_blocks ((En, pos) :: rest) [] bad = check_blocks rest [] (pos :: bad)
+      | check_blocks ((En, _) :: rest) (_ :: pending) bad = check_blocks rest pending bad
+      | check_blocks (_ :: rest) pending bad = check_blocks rest pending bad;
 
     fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
-      | add_args [] _ _ = err "Too many precedences"
-      | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
-          cons_fst arg (add_args syms ty ps)
-      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
-          cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
-      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
-          cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
-      | add_args (Argument _ :: _) _ _ = err "More arguments than in corresponding type"
-      | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
+      | add_args [] _ _ = err_in_mixfix "Too many precedences"
+      | add_args ((sym as (Argument ("index", _), _)) :: syms) ty ps =
+          add_args syms ty ps |>> cons sym
+      | add_args ((Argument _, pos) :: syms) (Type ("fun", [ty, tys])) [] =
+          add_args syms tys [] |>> cons (Argument (typ_to_nonterm ty, 0), pos)
+      | add_args ((Argument _, pos) :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
+          add_args syms tys ps |>> cons (Argument (typ_to_nonterm ty, p), pos)
+      | add_args ((Argument _, _) :: _) _ _ =
+          err_in_mixfix "More arguments than in corresponding type"
+      | add_args (sym :: syms) ty ps = add_args syms ty ps |>> cons sym;
+
+    fun logical_args (a as (Argument (s, p))) =
+          if s <> "prop" andalso member (op =) logical_types s then Argument ("logic", p) else a
+      | logical_args a = a;
 
     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
       | rem_pri sym = sym;
 
-    fun logify_types (a as (Argument (s, p))) =
-          if s <> "prop" andalso is_logtype s then Argument ("logic", p) else a
-      | logify_types a = a;
+    val indexes = filter (is_index o #1) symbs0;
+    val _ =
+      if length indexes <= 1 then ()
+      else error ("More than one index argument" ^ Position.here_list (map #2 indexes));
 
-
-    val raw_symbs = read_mfix sy handle ERROR msg => err msg;
-    val args = filter (fn Argument _ => true | _ => false) raw_symbs;
+    val args = map_filter (fn (arg as Argument _, _) => SOME arg | _ => NONE) symbs0;
     val (const', typ', syntax_consts, parse_rules) =
       if not (exists is_index args) then (const, typ, NONE, NONE)
       else
         let
           val indexed_const =
             if const <> "" then const ^ "_indexed"
-            else err "Missing constant name for indexed syntax";
+            else err_in_mixfix "Missing constant name for indexed syntax";
           val rangeT = Term.range_type typ handle Match =>
-            err "Missing structure argument for indexed syntax";
+            err_in_mixfix "Missing structure argument for indexed syntax";
 
           val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
           val (xs1, xs2) = chop (find_index is_index args) xs;
           val i = Ast.Variable "i";
-          val lhs = Ast.mk_appl (Ast.Constant indexed_const)
-            (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
+          val lhs =
+            Ast.mk_appl (Ast.Constant indexed_const)
+              (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
           val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
         in (indexed_const, rangeT, SOME (indexed_const, const), SOME (lhs, rhs)) end;
 
-    val (symbs, lhs) = add_args raw_symbs typ' pris;
+    val (symbs1, lhs) = add_args symbs0 typ' pris;
 
     val copy_prod =
       (lhs = "prop" orelse lhs = "logic")
         andalso const <> ""
-        andalso not (null symbs)
-        andalso not (exists is_delim symbs);
+        andalso not (null symbs1)
+        andalso not (exists (is_delim o #1) symbs1);
     val lhs' =
-      if copy_prod orelse lhs = "prop" andalso symbs = [Argument ("prop'", 0)] then lhs
+      if copy_prod orelse lhs = "prop" andalso map #1 symbs1 = [Argument ("prop'", 0)] then lhs
       else if lhs = "prop" then "prop'"
-      else if is_logtype lhs then "logic"
+      else if member (op =) logical_types lhs then "logic"
       else lhs;
-    val symbs' = map logify_types symbs;
-    val xprod = XProd (lhs', symbs', const', pri);
+    val symbs2 = map (apfst logical_args) symbs1;
 
-    val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
+    val _ =
+      (pri :: pris) |> List.app (fn p =>
+        if p >= 0 andalso p <= 1000 then ()
+        else err_in_mixfix ("Precedence " ^ string_of_int p ^ " out of range"));
+    val _ =
+      (case check_blocks symbs2 [] [] of
+        [] => ()
+      | bad => error ("Unbalanced block parentheses" ^ Position.here_list bad));
+
+    val xprod = XProd (lhs', map #1 symbs2, const', pri);
     val xprod' =
-      if Lexicon.is_terminal lhs' then err ("Illegal lhs " ^ quote lhs')
+      if Lexicon.is_terminal lhs' then
+        err_in_mixfix ("Illegal use of terminal " ^ quote lhs' ^ " as nonterminal")
       else if const <> "" then xprod
-      else if length (filter is_argument symbs') <> 1 then
-        err "Copy production must have exactly one argument"
-      else if exists is_terminal symbs' then xprod
-      else XProd (lhs', map rem_pri symbs', "", chain_pri);
+      else if length (filter (is_argument o #1) symbs2) <> 1 then
+        err_in_mixfix "Copy production must have exactly one argument"
+      else if exists (is_terminal o #1) symbs2 then xprod
+      else XProd (lhs', map (rem_pri o #1) symbs2, "", chain_pri);
 
   in (xprod', syntax_consts, parse_rules) end;
 
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -624,7 +624,7 @@
             else Syntax.const "_free" $ t
           end
       | mark (t as Var (xi, T)) =
-          if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
+          if xi = Auto_Bind.dddot then Const ("_DDDOT", T)
           else Syntax.const "_var" $ t
       | mark a = a;
   in mark tm end;
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -184,11 +184,6 @@
   | type_tr ts = raise TERM ("type_tr", ts);
 
 
-(* dddot *)
-
-fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts);
-
-
 (* quote / antiquote *)
 
 fun antiquote_tr name =
@@ -495,7 +490,6 @@
   ("_ofclass", fn _ => ofclass_tr),
   ("_sort_constraint", fn _ => sort_constraint_tr),
   ("_TYPE", fn _ => type_tr),
-  ("_DDDOT", fn _ => dddot_tr),
   ("_update_name", fn _ => update_name_tr),
   ("_index", fn _ => index_tr),
   ("_struct", struct_tr)];
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Mar 30 23:47:12 2016 +0200
@@ -417,6 +417,6 @@
     def heap(name: String): Path =
       find_heap(name) getOrElse
         error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
-          cat_lines(input_dirs.map(dir => "  " + dir.implode)))
+          cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
   }
 }
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/pure_thy.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -23,7 +23,6 @@
 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);
@@ -36,7 +35,7 @@
   ("_appl", typ "('b => 'a) => args => aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
 
 val applC_syntax =
- [("",       typ "'a => cargs",                  delimfix "_"),
+ [("",       typ "'a => cargs",                  Mixfix.mixfix "_"),
   ("_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))];
@@ -87,99 +86,99 @@
         "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 "'(_')"),
+   [("",            typ "prop' => prop",               Mixfix.mixfix "_"),
+    ("",            typ "logic => any",                Mixfix.mixfix "_"),
+    ("",            typ "prop' => any",                Mixfix.mixfix "_"),
+    ("",            typ "logic => logic",              Mixfix.mixfix "'(_')"),
+    ("",            typ "prop' => prop'",              Mixfix.mixfix "'(_')"),
     ("_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 "_"),
+    ("",            typ "tid_position => type",        Mixfix.mixfix "_"),
+    ("",            typ "tvar_position => type",       Mixfix.mixfix "_"),
+    ("",            typ "type_name => type",           Mixfix.mixfix "_"),
+    ("_type_name",  typ "id => type_name",             Mixfix.mixfix "_"),
+    ("_type_name",  typ "longid => type_name",         Mixfix.mixfix "_"),
     ("_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 "_,_"),
+    ("",            typ "class_name => sort",          Mixfix.mixfix "_"),
+    ("_class_name", typ "id => class_name",            Mixfix.mixfix "_"),
+    ("_class_name", typ "longid => class_name",        Mixfix.mixfix "_"),
+    ("_topsort",    typ "sort",                        Mixfix.mixfix "{}"),
+    ("_sort",       typ "classes => sort",             Mixfix.mixfix "{_}"),
+    ("",            typ "class_name => classes",       Mixfix.mixfix "_"),
+    ("_classes",    typ "class_name => classes => classes", Mixfix.mixfix "_,_"),
     ("_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 "_,/ _"),
+    ("_tappl",      typ "type => types => type_name => type", Mixfix.mixfix "((1'(_,/ _')) _)"),
+    ("",            typ "type => types",               Mixfix.mixfix "_"),
+    ("_types",      typ "type => types => types",      Mixfix.mixfix "_,/ _"),
     ("\<^type>fun", typ "type => type => type",        mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
     ("_bracket",    typ "types => type => type",       mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
-    ("",            typ "type => type",                delimfix "'(_')"),
-    ("\<^type>dummy", typ "type",                      delimfix "'_"),
+    ("",            typ "type => type",                Mixfix.mixfix "'(_')"),
+    ("\<^type>dummy", typ "type",                      Mixfix.mixfix "'_"),
     ("_type_prop",  typ "'a",                          NoSyn),
     ("_lambda",     typ "pttrns => 'a => logic",       mixfix ("(3\<lambda>_./ _)", [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 "'_"),
+    ("",            typ "'a => args",                  Mixfix.mixfix "_"),
+    ("_args",       typ "'a => args => args",          Mixfix.mixfix "_,/ _"),
+    ("",            typ "id_position => idt",          Mixfix.mixfix "_"),
+    ("_idtdummy",   typ "idt",                         Mixfix.mixfix "'_"),
     ("_idtyp",      typ "id_position => type => idt",  mixfix ("_::_", [], 0)),
     ("_idtypdummy", typ "type => idt",                 mixfix ("'_()::_", [], 0)),
-    ("",            typ "idt => idt",                  delimfix "'(_')"),
-    ("",            typ "idt => idts",                 delimfix "_"),
+    ("",            typ "idt => idt",                  Mixfix.mixfix "'(_')"),
+    ("",            typ "idt => idts",                 Mixfix.mixfix "_"),
     ("_idts",       typ "idt => idts => idts",         mixfix ("_/ _", [1, 0], 0)),
-    ("",            typ "idt => pttrn",                delimfix "_"),
-    ("",            typ "pttrn => pttrns",             delimfix "_"),
+    ("",            typ "idt => pttrn",                Mixfix.mixfix "_"),
+    ("",            typ "pttrn => pttrns",             Mixfix.mixfix "_"),
     ("_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 "\<dots>"),
-    ("_aprop",      typ "aprop => prop",               delimfix "PROP _"),
-    ("_asm",        typ "prop => asms",                delimfix "_"),
-    ("_asms",       typ "prop => asms => asms",        delimfix "_;/ _"),
+    ("",            typ "aprop => aprop",              Mixfix.mixfix "'(_')"),
+    ("",            typ "id_position => aprop",        Mixfix.mixfix "_"),
+    ("",            typ "longid_position => aprop",    Mixfix.mixfix "_"),
+    ("",            typ "var_position => aprop",       Mixfix.mixfix "_"),
+    ("_DDDOT",      typ "aprop",                       Mixfix.mixfix "\<dots>"),
+    ("_aprop",      typ "aprop => prop",               Mixfix.mixfix "PROP _"),
+    ("_asm",        typ "prop => asms",                Mixfix.mixfix "_"),
+    ("_asms",       typ "prop => asms => asms",        Mixfix.mixfix "_;/ _"),
     ("_bigimpl",    typ "asms => prop => prop",        mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
-    ("_ofclass",    typ "type => logic => prop",       delimfix "(1OFCLASS/(1'(_,/ _')))"),
+    ("_ofclass",    typ "type => logic => prop",       Mixfix.mixfix "(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 "\<dots>"),
+    ("_TYPE",       typ "type => logic",               Mixfix.mixfix "(1TYPE/(1'(_')))"),
+    ("",            typ "id_position => logic",        Mixfix.mixfix "_"),
+    ("",            typ "longid_position => logic",    Mixfix.mixfix "_"),
+    ("",            typ "var_position => logic",       Mixfix.mixfix "_"),
+    ("_DDDOT",      typ "logic",                       Mixfix.mixfix "\<dots>"),
     ("_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 "'\<index>"),
+    ("_position",   typ "num_token => num_position",   Mixfix.mixfix "_"),
+    ("_position",   typ "float_token => float_position", Mixfix.mixfix "_"),
+    ("_constify",   typ "num_position => num_const",   Mixfix.mixfix "_"),
+    ("_constify",   typ "float_position => float_const", Mixfix.mixfix "_"),
+    ("_index",      typ "logic => index",              Mixfix.mixfix "(00\<^bsub>_\<^esub>)"),
+    ("_indexdefault", typ "index",                     Mixfix.mixfix ""),
+    ("_indexvar",   typ "index",                       Mixfix.mixfix "'\<index>"),
     ("_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",      Mixfix.mixfix "_"),
+    ("_position_sort", typ "tvar => tvar_position",    Mixfix.mixfix "_"),
+    ("_position",   typ "id => id_position",           Mixfix.mixfix "_"),
+    ("_position",   typ "longid => longid_position",   Mixfix.mixfix "_"),
+    ("_position",   typ "var => var_position",         Mixfix.mixfix "_"),
+    ("_position",   typ "str_token => str_position",   Mixfix.mixfix "_"),
+    ("_position",   typ "string_token => string_position", Mixfix.mixfix "_"),
+    ("_position",   typ "cartouche => cartouche_position", Mixfix.mixfix "_"),
     ("_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 _"),
+    ("_context_const", typ "id_position => logic",     Mixfix.mixfix "CONST _"),
+    ("_context_const", typ "id_position => aprop",     Mixfix.mixfix "CONST _"),
+    ("_context_const", typ "longid_position => logic", Mixfix.mixfix "CONST _"),
+    ("_context_const", typ "longid_position => aprop", Mixfix.mixfix "CONST _"),
+    ("_context_xconst", typ "id_position => logic",    Mixfix.mixfix "XCONST _"),
+    ("_context_xconst", typ "id_position => aprop",    Mixfix.mixfix "XCONST _"),
+    ("_context_xconst", typ "longid_position => logic", Mixfix.mixfix "XCONST _"),
+    ("_context_xconst", typ "longid_position => aprop", Mixfix.mixfix "XCONST _"),
+    (const "Pure.dummy_pattern", typ "aprop",          Mixfix.mixfix "'_"),
+    ("_sort_constraint", typ "type => prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
+    (const "Pure.term", typ "logic => prop",           Mixfix.mixfix "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)
@@ -189,9 +188,9 @@
     (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 "..."),
+    ("_DDDOT",            typ "aprop",                  Mixfix.mixfix "..."),
     ("_bigimpl",          typ "asms => prop => prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
-    ("_DDDOT",            typ "logic",                  delimfix "...")]
+    ("_DDDOT",            typ "logic",                  Mixfix.mixfix "...")]
   #> Sign.add_syntax ("", false)
    [(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))]
   #> Sign.add_consts
@@ -200,7 +199,7 @@
     (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", binder ("\<And>", 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", Mixfix.mixfix "'_")]
   #> 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"]) []
diff -r d4b7d128ec5a -r 42a997773bb0 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Pure/variable.ML	Wed Mar 30 23:47:12 2016 +0200
@@ -230,6 +230,9 @@
 
 (* constraints *)
 
+fun constrain_var (xi, T) =
+  if T = dummyT then Vartab.delete_safe xi else Vartab.update (xi, T);
+
 fun constrain_tvar (xi, raw_S) =
   let val S = #2 (Term_Position.decode_positionS raw_S)
   in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end;
@@ -237,8 +240,8 @@
 fun declare_constraints t = map_constraints (fn (types, sorts) =>
   let
     val types' = fold_aterms
-      (fn Free (x, T) => Vartab.update ((x, ~1), T)
-        | Var v => Vartab.update v
+      (fn Free (x, T) => constrain_var ((x, ~1), T)
+        | Var v => constrain_var v
         | _ => I) t types;
     val sorts' = (fold_types o fold_atyps)
       (fn TFree (x, S) => constrain_tvar ((x, ~1), S)
diff -r d4b7d128ec5a -r 42a997773bb0 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Wed Mar 30 23:47:12 2016 +0200
@@ -13,7 +13,7 @@
 plugin.isabelle.jedit.Plugin.usePluginHome=false
 
 #dependencies
-plugin.isabelle.jedit.Plugin.depend.0=jdk 1.7
+plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8
 plugin.isabelle.jedit.Plugin.depend.1=jedit 05.03.00.00
 plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
 plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
diff -r d4b7d128ec5a -r 42a997773bb0 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 30 15:16:50 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 30 23:47:12 2016 +0200
@@ -568,7 +568,8 @@
               else "breakpoint (disabled)"
             Some(add(prev, r, (true, XML.Text(text))))
           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
-            Some(add(prev, r, (true, XML.Text("language: " + language))))
+            val lang = Word.implode(Word.explode('_', language))
+            Some(add(prev, r, (true, XML.Text("language: " + lang))))
 
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
             Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))