# HG changeset patch
# User wenzelm
# Date 1285248963 -7200
# Node ID 108901b4921077a3449377fbc1251d679bc838b0
# Parent  a5d0bcfb95a329cf3d856f5c2899cd62bc31da7d
tuned;

diff -r a5d0bcfb95a3 -r 108901b49210 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Thu Sep 23 15:21:04 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 23 15:36:03 2010 +0200
@@ -99,14 +99,16 @@
 
   def is_state(msg: XML.Tree): Boolean =
     msg match {
-      case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+      case XML.Elem(Markup(Markup.WRITELN, _),
+        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
       case _ => false
     }
 
 
   /* reported positions */
 
-  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+  private val include_pos =
+    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   {
@@ -129,9 +131,6 @@
 
 trait Isar_Document extends Isabelle_Process
 {
-  import Isar_Document._
-
-
   /* commands */
 
   def define_command(id: Document.Command_ID, text: String): Unit =