--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 24 18:12:41 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 24 22:41:08 2014 +0100
@@ -109,7 +109,7 @@
Mixfix (step_mixfix (), [1000], 1000)) thy
in
(pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
- Proof_Context.transfer_syntax thy ctxt)
+ Proof_Context.transfer thy ctxt)
end
(** Term reconstruction **)
--- a/src/Pure/General/table.ML Mon Feb 24 18:12:41 2014 +0100
+++ b/src/Pure/General/table.ML Mon Feb 24 22:41:08 2014 +0100
@@ -368,8 +368,13 @@
fun make entries = fold update_new entries empty;
fun join f (table1, table2) =
- let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
- in if pointer_eq (table1, table2) then table1 else fold_table add table2 table1 end;
+ let
+ fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
+ in
+ if pointer_eq (table1, table2) then table1
+ else if is_empty table1 then table2
+ else fold_table add table2 table1
+ end;
fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);
--- a/src/Pure/Isar/locale.ML Mon Feb 24 18:12:41 2014 +0100
+++ b/src/Pure/Isar/locale.ML Mon Feb 24 22:41:08 2014 +0100
@@ -36,6 +36,7 @@
declaration list ->
(string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
(string * morphism) list -> theory -> theory
+ val intern: theory -> xstring -> string
val check: theory -> xstring * Position.T -> string
val extern: theory -> string -> xstring
val markup_name: Proof.context -> string -> string
@@ -159,6 +160,7 @@
val merge = Name_Space.join_tables (K merge_locale);
);
+val intern = Name_Space.intern o #1 o Locales.get;
fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
--- a/src/Pure/Isar/proof_context.ML Mon Feb 24 18:12:41 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Feb 24 22:41:08 2014 +0100
@@ -50,7 +50,6 @@
val extern_const: Proof.context -> string -> xstring
val markup_const: Proof.context -> string -> string
val pretty_const: Proof.context -> string -> Pretty.T
- val transfer_syntax: theory -> Proof.context -> Proof.context
val transfer: theory -> Proof.context -> Proof.context
val background_theory: (theory -> theory) -> Proof.context -> Proof.context
val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
--- a/src/Pure/Proof/proof_syntax.ML Mon Feb 24 18:12:41 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Mon Feb 24 22:41:08 2014 +0100
@@ -246,7 +246,7 @@
fun pretty_proof ctxt prf =
Proof_Context.pretty_term_abbrev
- (Proof_Context.transfer_syntax (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
+ (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
(term_of_proof prf);
fun pretty_proof_of ctxt full th =
--- a/src/Tools/jEdit/etc/options Mon Feb 24 18:12:41 2014 +0100
+++ b/src/Tools/jEdit/etc/options Mon Feb 24 22:41:08 2014 +0100
@@ -85,7 +85,7 @@
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"
option keyword3_color : string = "0099FFFF"
-option caret_invisible_color : string = "99999980"
+option caret_invisible_color : string = "50000080"
option tfree_color : string = "A020F0FF"
option tvar_color : string = "A020F0FF"
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Feb 24 18:12:41 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Feb 24 22:41:08 2014 +0100
@@ -456,6 +456,7 @@
{
robust_rendering { rendering =>
val caret_range = get_caret_range(true)
+ val caret_color = text_area.getPainter.getCaretColor
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
@@ -494,7 +495,7 @@
if (!hyperlink_area.is_active) {
def paint_completion(range: Text.Range) {
for (r <- JEdit_Lib.gfx_range(text_area, range)) {
- gfx.setColor(get_caret_color(rendering))
+ gfx.setColor(caret_color)
gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
}
}