Re: [isabelle] 2014-RC1 issues: Duplicate annotations



Hi,

in some cases, duplicate annotations occur in terms in proof_methods.
Consider the theory:

lemma P
  apply (simp add: exI[of _ 1])

and hover over the 1, which now has a duplicate set of annotations.

Duplicate annotations also occur in locale expressions:

locale A = fixes x
locale B = A z for z + assumes False

Here, the "z" has a duplicate set of annotations from Syntax.check_term
(but only a single one from Syntax.read_term).



I tried to dig into what triggers this behaviour:

For proof methods, this is related to the introduction of a method
closure (which executes every proof method twice). The use of e.g. the
Args.term parser is fine; but if one uses Args.name_inner_syntax and
Syntax.read_term later, annotations are duplicated:

method_setup foo1 = ‹
  Args.term >> (fn _ => fn _ => SIMPLE_METHOD' (K all_tac))
›

vs.

method_setup foo2 = ‹
  Scan.peek (fn ctxt => Args.name_inner_syntax >> Syntax.read_term
(Context.proof_of ctxt)) >>
  (fn _ => fn _ => SIMPLE_METHOD' (K all_tac))
›

except if the method errors out unconditionally (and hence is called
only once):

method_setup foo3 = ‹
  Args.term -- Scan.peek (fn ctxt => Args.name_inner_syntax >>
Syntax.read_term (Context.proof_of ctxt)) >>
  (fn _ => raise Match)
›

  -- Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.