--- a/src/Pure/Isar/generic_target.ML Wed Mar 30 17:03:26 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML Wed Mar 30 19:25:04 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*)
@@ -97,17 +98,24 @@
in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
fun check_mixfix ctxt (b, extra_tfrees) mx =
- if null extra_tfrees then mx
- else
- (if Context_Position.is_visible ctxt then
- warning
- ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
- commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
- (if Mixfix.is_empty mx then ""
- else
- "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx) ^
- Position.here (Mixfix.pos_of mx)))
- else (); NoSyn);
+ let
+ val visible = Context_Position.is_visible ctxt;
+ val _ =
+ ctxt |> Proof_Context.add_fixes
+ [(Binding.reset_pos b, NONE, if visible then mx else Mixfix.reset_pos mx)];
+ val mx' =
+ if null extra_tfrees then mx
+ else
+ (if visible then
+ warning
+ ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
+ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
+ (if Mixfix.is_empty mx then ""
+ else
+ "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx) ^
+ Position.here (Mixfix.pos_of mx)))
+ else (); NoSyn);
+ in Mixfix.reset_pos mx' end;
fun check_mixfix_global (b, no_params) mx =
if no_params orelse Mixfix.is_empty mx then mx
@@ -148,10 +156,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 +357,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/Syntax/syntax_ext.ML Wed Mar 30 17:03:26 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Wed Mar 30 19:25:04 2016 +0200
@@ -99,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 **)
@@ -156,16 +164,21 @@
Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
val scan_symb =
- Symbol_Pos.scan_pos -- scan_sym >> (SOME o swap) ||
+ 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 (~$$ "'");
in
-val read_mfix = map_filter I o the o Scan.read Symbol_Pos.stopper scan_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 #1) 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;
@@ -177,6 +190,8 @@
fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
let
+ val symbs0 = read_mfix sy;
+
fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
fun check_blocks [] pending bad = pending @ bad
@@ -204,15 +219,12 @@
fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
| rem_pri sym = sym;
-
- val raw_symbs = read_mfix sy;
-
- val indexes = filter (is_index o #1) raw_symbs;
+ 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 args = map_filter (fn (arg as Argument _, _) => SOME arg | _ => NONE) 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
@@ -232,38 +244,38 @@
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 o #1) symbs);
+ andalso not (null symbs1)
+ andalso not (exists (is_delim o #1) symbs1);
val lhs' =
- if copy_prod orelse lhs = "prop" andalso map #1 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 member (op =) logical_types lhs then "logic"
else lhs;
- val symbs' = map (apfst logical_args) symbs;
+ val symbs2 = map (apfst logical_args) symbs1;
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 symbs' [] [] of
+ (case check_blocks symbs2 [] [] of
[] => ()
| bad => error ("Unbalanced block parentheses" ^ Position.here_list bad));
- val xprod = XProd (lhs', map #1 symbs', const', pri);
+ val xprod = XProd (lhs', map #1 symbs2, const', pri);
val xprod' =
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 o #1) symbs') <> 1 then
+ 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) symbs' then xprod
- else XProd (lhs', map (rem_pri o #1) symbs', "", chain_pri);
+ 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;