# HG changeset patch # User wenzelm # Date 1459358704 -7200 # Node ID ff3b8e4079bd57c453b1760c14f83da491b3544e # Parent 3e9a68bd30a77b1d969d5963960b959dc2080f47 more PIDE markup; tuned; diff -r 3e9a68bd30a7 -r ff3b8e4079bd src/Pure/Isar/generic_target.ML --- 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 **) diff -r 3e9a68bd30a7 -r ff3b8e4079bd src/Pure/Syntax/syntax_ext.ML --- 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;