# HG changeset patch
# User immler@in.tum.de
# Date 1251384096 -7200
# Node ID 1310dc269b4a64665c8ae0c613f2362dbdff9db4
# Parent  c3693cca5a046915975955557f7b5c77c5cc6685
lazy fields

diff -r c3693cca5a04 -r 1310dc269b4a src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Thu Aug 27 16:41:36 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Thu Aug 27 16:41:36 2009 +0200
@@ -121,33 +121,14 @@
       }, "style")
   }
 
-  def markup_root: MarkupNode = {
-    val cmd_markup_root = cmd.state.markup_root
-    (cmd_markup_root /: state.markup_root.children) (_ + _)
-  }
+  def markup_root: MarkupNode =
+    (cmd.state.markup_root /: state.markup_root.children) (_ + _)
 
-  def highlight_node: MarkupNode =
-  {
-    import MarkupNode._
-    markup_root.filter(_.info match {
-      case RootInfo() | HighlightInfo(_) => true
-      case _ => false
-    }).head
-  }
+  def type_at(pos: Int): String = state.type_at(pos)
 
-  def type_at(pos: Int): String =
-  {
-    val types = state.markup_root.
-      filter(_.info match { case TypeInfo(_) => true case _ => false })
-    types.flatten(_.flatten).
-    find(t => t.start <= pos && t.stop > pos).
-    map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })).
-    getOrElse(null)
-  }
+  def ref_at(pos: Int): Option[MarkupNode] = state.ref_at(pos)
 
-  def ref_at(pos: Int): Option[MarkupNode] =
-    state.markup_root.
-      filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
-      flatten(_.flatten).
-      find(t => t.start <= pos && t.stop > pos)
-}
+  def highlight_node =
+    (cmd.state.highlight_node /: state.highlight_node.children) (_ + _)
+
+}
\ No newline at end of file
diff -r c3693cca5a04 -r 1310dc269b4a src/Tools/jEdit/src/prover/State.scala
--- a/src/Tools/jEdit/src/prover/State.scala	Thu Aug 27 16:41:36 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala	Thu Aug 27 16:41:36 2009 +0200
@@ -28,21 +28,40 @@
     State(cmd, status, results + res, markup_root)
   private def add_markup(markup: MarkupNode):State =
     State(cmd, status, results, markup_root + markup)
+
   /* markup */
+  lazy val highlight_node: MarkupNode =
+  {
+    import MarkupNode._
+    markup_root.filter(_.info match {
+      case RootInfo() | HighlightInfo(_) => true
+      case _ => false
+    }).head
+  }
+
+  lazy private val types =
+    markup_root.filter(_.info match {
+      case TypeInfo(_) => true
+      case _ => false }).flatten(_.flatten)
 
   def type_at(pos: Int): String =
   {
-    val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
-    types.flatten(_.flatten).
-      find(t => t.start <= pos && t.stop > pos).
-      map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })).
+    types.find(t => t.start <= pos && t.stop > pos).map(t =>
+      t.content + ": " + (t.info match {
+        case TypeInfo(i) => i
+        case _ => "" })).
       getOrElse(null)
   }
 
+  lazy private val refs =
+    markup_root.filter(_.info match {
+      case RefInfo(_, _, _, _) => true
+      case _ => false }).flatten(_.flatten)
+
   def ref_at(pos: Int): Option[MarkupNode] =
-    markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
-      flatten(_.flatten).
-      find(t => t.start <= pos && t.stop > pos)
+    refs.find(t => t.start <= pos && t.stop > pos)
+
+
 
   def +(message: XML.Tree) = {
     val changed: State =