--- 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
--- 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
--- 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
--- 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 () =
--- 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;
--- 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;
-
--- 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;
--- 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 =
--- 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 **)
--- 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 =
--- 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;
--- 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;
--- 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
--- 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)];
--- 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 *)
--- 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)),
--- 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
--- 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
--- 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;
--- 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;
--- 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)];
--- 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)))
}
}
--- 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"]) []
--- 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)
--- 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
--- 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"))))