# HG changeset patch
# User wenzelm
# Date 1393278068 -3600
# Node ID 3244957ca236a204a6dee685f79f8f9229ce644d
# Parent  7572fc374f8029d692d202095afb5f8da359ba8a# Parent  aaf024d63b351dff99f82376a758c93df80af7b8
merged

diff -r 7572fc374f80 -r 3244957ca236 src/HOL/Tools/Nitpick/nitpick_model.ML
--- 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 **)
diff -r 7572fc374f80 -r 3244957ca236 src/Pure/General/table.ML
--- 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);
 
diff -r 7572fc374f80 -r 3244957ca236 src/Pure/Isar/locale.ML
--- 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));
diff -r 7572fc374f80 -r 3244957ca236 src/Pure/Isar/proof_context.ML
--- 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
diff -r 7572fc374f80 -r 3244957ca236 src/Pure/Proof/proof_syntax.ML
--- 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 =
diff -r 7572fc374f80 -r 3244957ca236 src/Tools/jEdit/etc/options
--- 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"
diff -r 7572fc374f80 -r 3244957ca236 src/Tools/jEdit/src/rich_text_area.scala
--- 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)
                 }
               }