# HG changeset patch
# User haftmann
# Date 1315243118 -7200
# Node ID 27fb2285bdeeb3214158a0fb9e83b1cbbb8c1d2e
# Parent  487ae6317f7bca261a4e0c5bbb0e04344d665c4b# Parent  4ea8489593402176f8c64476fb32880c0e855cc5
merged

diff -r 4ea848959340 -r 27fb2285bdee src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Sep 05 07:49:31 2011 +0200
+++ b/src/HOL/Int.thy	Mon Sep 05 19:18:38 2011 +0200
@@ -446,6 +446,12 @@
 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
 done
 
+lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> of_nat n"
+  by (cases x, simp add: nat le int_def le_diff_conv)
+
+lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
+  by (cases x, cases y, simp add: nat le)
+
 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
 by(simp add: nat_eq_iff) arith
 
diff -r 4ea848959340 -r 27fb2285bdee src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Mon Sep 05 07:49:31 2011 +0200
+++ b/src/HOL/RComplete.thy	Mon Sep 05 19:18:38 2011 +0200
@@ -336,9 +336,6 @@
 lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
   unfolding natfloor_def by simp
 
-lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
-  by simp (* TODO: move to Int.thy *)
-
 lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
   unfolding natfloor_def by (intro nat_mono floor_mono)
 
@@ -474,9 +471,6 @@
 lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
   unfolding natceiling_def by (intro nat_mono ceiling_mono)
 
-lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
-  by auto (* TODO: move to Int.thy *)
-
 lemma natceiling_le: "x <= real a ==> natceiling x <= a"
   unfolding natceiling_def real_of_nat_def
   by (simp add: nat_le_iff ceiling_le_iff)
diff -r 4ea848959340 -r 27fb2285bdee src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Mon Sep 05 07:49:31 2011 +0200
+++ b/src/Pure/General/xml.scala	Mon Sep 05 19:18:38 2011 +0200
@@ -159,6 +159,7 @@
           case Cache_Markup(x, f) => f(cache_markup(x))
           case Cache_Tree(x, f) => f(cache_tree(x))
           case Cache_Body(x, f) => f(cache_body(x))
+          case Cache_Ignore(x, f) => f(x)
           case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad)
         }
       }
@@ -168,12 +169,14 @@
     private case class Cache_Markup(x: Markup, f: Markup => Unit)
     private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit)
     private case class Cache_Body(x: XML.Body, f: XML.Body => Unit)
+    private case class Cache_Ignore[A](x: A, f: A => Unit)
 
     // main methods
     def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) }
     def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) }
     def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) }
     def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) }
+    def cache_ignore[A](x: A)(f: A => Unit) { cache_actor ! Cache_Ignore(x, f) }
   }
 
 
diff -r 4ea848959340 -r 27fb2285bdee src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Sep 05 07:49:31 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Sep 05 19:18:38 2011 +0200
@@ -99,7 +99,8 @@
   {
     if (kind == Markup.INIT) rm_fifos()
     if (kind == Markup.RAW)
-      receiver ! new Result(XML.Elem(Markup(kind, props), body))
+      xml_cache.cache_ignore(
+        new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result)
     else {
       val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
       xml_cache.cache_tree(msg)((message: XML.Tree) =>