--- a/src/HOL/Quotient.thy Mon Jun 28 11:04:02 2010 +0200
+++ b/src/HOL/Quotient.thy Mon Jun 28 13:36:21 2010 +0200
@@ -768,7 +768,7 @@
{* lifts theorems to quotient types *}
method_setup lifting_setup =
- {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
+ {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
{* sets up the three goals for the quotient lifting procedure *}
method_setup regularize =
--- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Jun 28 11:04:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Jun 28 13:36:21 2010 +0200
@@ -50,6 +50,7 @@
let
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+ val _ = if is_Const rhs then () else warning "The definiens is not a constant"
fun sanity_test NONE _ = true
| sanity_test (SOME bind) str =
@@ -91,7 +92,7 @@
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
let
val rty = fastype_of rconst
- val qty = derive_qtyp qtys rty ctxt
+ val qty = derive_qtyp qtys rty false ctxt
val lhs = Free (qconst_name, qty)
in
quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jun 28 11:04:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jun 28 13:36:21 2010 +0200
@@ -11,7 +11,7 @@
val injection_tac: Proof.context -> int -> tactic
val all_injection_tac: Proof.context -> int -> tactic
val clean_tac: Proof.context -> int -> tactic
- val procedure_tac: Proof.context -> thm -> int -> tactic
+ val procedure_tac: Proof.context -> thm list -> int -> tactic
val lift_tac: Proof.context -> thm list -> int -> tactic
val quotient_tac: Proof.context -> int -> tactic
val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
@@ -620,12 +620,23 @@
Object_Logic.full_atomize_tac
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
- let
- val rthm' = atomize_thm rthm
- val rule = procedure_inst ctxt (prop_of rthm') goal
- in
- (rtac rule THEN' rtac rthm') i
- end)
+ case rthm of
+ [] =>
+ let
+ val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+ val rtrm = derive_qtrm qtys goal true ctxt
+ val rule = procedure_inst ctxt rtrm goal
+ in
+ rtac rule i
+ end
+ | [rthm'] =>
+ let
+ val rthm'' = atomize_thm rthm'
+ val rule = procedure_inst ctxt (prop_of rthm'') goal
+ in
+ (rtac rule THEN' rtac rthm'') i
+ end
+ | _ => error "more than one raw theorem given")
(* Automatic Proofs *)
@@ -633,14 +644,24 @@
fun lift_tac ctxt rthms =
let
fun mk_tac rthm =
- procedure_tac ctxt rthm
+ procedure_tac ctxt [rthm]
THEN' RANGE
[regularize_tac ctxt,
all_injection_tac ctxt,
+ clean_tac ctxt];
+ val mk_tac_raw =
+ procedure_tac ctxt []
+ THEN' RANGE
+ [fn _ => all_tac,
+ regularize_tac ctxt,
+ all_injection_tac ctxt,
clean_tac ctxt]
in
simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
- THEN' RANGE (map mk_tac rthms)
+ THEN'
+ (case rthms of
+ [] => mk_tac_raw
+ | _ => RANGE (map mk_tac rthms))
end
fun lifted qtys ctxt thm =
@@ -649,7 +670,7 @@
so we do it both in the original theorem *)
val thm' = Drule.eta_contraction_rule thm
val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
- val goal = derive_qtrm qtys (prop_of thm'') ctxt'
+ val goal = derive_qtrm qtys (prop_of thm'') false ctxt'
in
Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
|> singleton (ProofContext.export ctxt' ctxt)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Mon Jun 28 11:04:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Jun 28 13:36:21 2010 +0200
@@ -26,8 +26,8 @@
val inj_repabs_trm: Proof.context -> term * term -> term
val inj_repabs_trm_chk: Proof.context -> term * term -> term
- val derive_qtyp: typ list -> typ -> Proof.context -> typ
- val derive_qtrm: typ list -> term -> Proof.context -> term
+ val derive_qtyp: typ list -> typ -> bool -> Proof.context -> typ
+ val derive_qtrm: typ list -> term -> bool -> Proof.context -> term
end;
structure Quotient_Term: QUOTIENT_TERM =
@@ -690,7 +690,7 @@
(*** Wrapper for automatically transforming an rthm into a qthm ***)
-(* subst_tys takes a list of (rty, qty) substitution pairs
+(* subst_rty takes a list of (rty, qty) substitution pairs
and replaces all occurences of rty in the given type
by an appropriate qty
*)
@@ -711,7 +711,7 @@
end
| _ => rty
-(* subst_trms takes a list of (rconst, qconst) substitution pairs,
+(* subst_rtrm takes a list of (rconst, qconst) substitution pairs,
as well as (rty, qty) substitution pairs, and replaces all
occurences of rconst and rty by appropriate instances of
qconst and qty
@@ -739,26 +739,29 @@
(* generates type substitutions out of the
types involved in a quotient
*)
-fun get_ty_subst qtys ctxt =
+fun get_ty_subst qtys reverse ctxt =
Quotient_Info.quotdata_dest ctxt
|> map (fn x => (#rtyp x, #qtyp x))
|> filter (fn (_, qty) => member (op =) qtys qty)
+ |> map (fn (x, y) => if reverse then (y, x) else (x, y))
(* generates term substitutions out of the qconst
definitions and relations in a quotient
*)
-fun get_trm_subst qtys ctxt =
-let
- val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys ctxt)
+fun get_trm_subst qtys reverse ctxt =
+let
+ val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys reverse ctxt)
fun proper (rt, qt) = (subst_rtyp' (fastype_of rt) = fastype_of qt)
-
+
val const_substs =
Quotient_Info.qconsts_dest ctxt
- |> map (fn x => (#rconst x, #qconst x))
+ |> map (fn x => (#rconst x, #qconst x))
+ |> map (fn (x, y) => if reverse then (y, x) else (x, y))
- val rel_substs =
+ val rel_substs =
Quotient_Info.quotdata_dest ctxt
|> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
+ |> map (fn (x, y) => if reverse then (y, x) else (x, y))
in
filter proper (const_substs @ rel_substs)
end
@@ -766,11 +769,11 @@
(* derives a qtyp and qtrm out of a rtyp and rtrm,
respectively
*)
-fun derive_qtyp qtys rty ctxt =
- subst_rtyp ctxt (get_ty_subst qtys ctxt) rty
+fun derive_qtyp qtys rty unlift ctxt =
+ subst_rtyp ctxt (get_ty_subst qtys unlift ctxt) rty
-fun derive_qtrm qtys rtrm ctxt =
- subst_rtrm ctxt (get_ty_subst qtys ctxt) (get_trm_subst qtys ctxt) rtrm
+fun derive_qtrm qtys rtrm unlift ctxt =
+ subst_rtrm ctxt (get_ty_subst qtys unlift ctxt) (get_trm_subst qtys unlift ctxt) rtrm
end; (* structure *)
--- a/src/Pure/General/symbol.scala Mon Jun 28 11:04:02 2010 +0200
+++ b/src/Pure/General/symbol.scala Mon Jun 28 13:36:21 2010 +0200
@@ -31,7 +31,9 @@
/* Symbol regexps */
private val plain = new Regex("""(?xs)
- [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+ [^\r\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+
+ private val newline = new Regex("""(?xs) \r\n | \r """)
private val symbol = new Regex("""(?xs)
\\ < (?:
@@ -39,17 +41,17 @@
\^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
// FIXME cover bad surrogates!?
- // FIXME check wrt. ML version
+ // FIXME check wrt. Isabelle/ML version
private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
""" \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
// total pattern
- val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
+ val regex = new Regex(plain + "|" + newline + "|" + symbol + "|" + bad_symbol + "| .")
/* basic matching */
- def is_plain(c: Char): Boolean = !(c == '\\' || '\ud800' <= c && c <= '\udfff')
+ def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
def is_wellformed(s: CharSequence): Boolean =
s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
--- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Jun 28 11:04:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jun 28 13:36:21 2010 +0200
@@ -56,6 +56,19 @@
class Document_Model(val session: Session, val buffer: Buffer)
{
+ /* visible line end */
+
+ // simplify slightly odd result of TextArea.getLineEndOffset
+ // NB: jEdit already normalizes \r\n and \r to \n
+ def visible_line_end(start: Int, end: Int): Int =
+ {
+ val end1 = end - 1
+ if (start <= end1 && end1 < buffer.getLength &&
+ buffer.getSegment(end1, 1).charAt(0) == '\n') end1
+ else end
+ }
+
+
/* history */
private val document_0 = session.begin_document(buffer.getName)
@@ -127,9 +140,11 @@
/* activation */
+ private val token_marker = new Isabelle_Token_Marker(this)
+
def activate()
{
- buffer.setTokenMarker(new Isabelle_Token_Marker(this))
+ buffer.setTokenMarker(token_marker)
buffer.addBufferListener(buffer_listener)
buffer.propertiesChanged()
@@ -137,6 +152,11 @@
edits_delay()
}
+ def refresh()
+ {
+ buffer.setTokenMarker(token_marker)
+ }
+
def deactivate()
{
buffer.setTokenMarker(buffer.getMode.getTokenMarker)
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Jun 28 11:04:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jun 28 13:36:21 2010 +0200
@@ -129,16 +129,20 @@
val document = model.recent_document()
def from_current(pos: Int) = model.from_current(document, pos)
def to_current(pos: Int) = model.to_current(document, pos)
- val metrics = text_area.getPainter.getFontMetrics
+
+ val line_end = model.visible_line_end(start, end)
+ val line_height = text_area.getPainter.getFontMetrics.getHeight
+
val saved_color = gfx.getColor
try {
for ((command, command_start) <-
- document.command_range(from_current(start), from_current(end)) if !command.is_ignored)
+ document.command_range(from_current(start), from_current(line_end)) if !command.is_ignored)
{
- val begin = start max to_current(command_start)
- val finish = (end - 1) min to_current(command_start + command.length)
- encolor(gfx, y, metrics.getHeight, begin, finish,
- Document_View.choose_color(document, command), true)
+ val p = text_area.offsetToXY(start max to_current(command_start))
+ val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
+ assert(p.y == q.y)
+ gfx.setColor(Document_View.choose_color(document, command))
+ gfx.fillRect(p.x, y, q.x - p.x, line_height)
}
}
finally { gfx.setColor(saved_color) }
@@ -205,26 +209,6 @@
text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
text_area.getLastPhysicalLine)
- private def encolor(gfx: Graphics2D,
- y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
- {
- val start = text_area.offsetToXY(begin)
- val stop =
- if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
- else {
- val p = text_area.offsetToXY(finish - 1)
- val metrics = text_area.getPainter.getFontMetrics
- p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
- p
- }
-
- if (start != null && stop != null) {
- gfx.setColor(color)
- if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
- else gfx.drawRect(start.x, y, stop.x - start.x, height)
- }
- }
-
/* overview of command status left of scrollbar */
--- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Jun 28 11:04:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Jun 28 13:36:21 2010 +0200
@@ -20,7 +20,7 @@
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
+import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.jedit.gui.DockableWindowManager
@@ -203,6 +203,13 @@
override def handleMessage(message: EBMessage)
{
message match {
+ case msg: BufferUpdate
+ if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+ Document_Model(msg.getBuffer) match {
+ case Some(model) => model.refresh()
+ case _ =>
+ }
+
case msg: EditPaneUpdate =>
val edit_pane = msg.getEditPane
val buffer = edit_pane.getBuffer