Re: [isabelle] 2014-RC1 issues



An issue with the precedence of warnings and errors:

Under certain circumstances, if a method emits a warning and the apply
fails (with an error), the line is only marked as a warning in the
theories panel and the right side bar.

Reconstruct with:

theory Scratch imports Main begin

method_setup foo = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (warning "warning"; tracing
"trace"; K no_tac))
›

lemma P apply foo

end

  -- Lars




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