# HG changeset patch
# User wenzelm
# Date 1251549099 -7200
# Node ID 375db037f4d26660a8b8ec9a78586b34b83c3613
# Parent  696d64ed85dad93f07934b37bd8c8d497a5535ed
misc tuning;

diff -r 696d64ed85da -r 375db037f4d2 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Aug 29 12:01:25 2009 +0200
+++ b/src/Pure/General/markup.scala	Sat Aug 29 14:31:39 2009 +0200
@@ -6,8 +6,9 @@
 
 package isabelle
 
-object Markup {
 
+object Markup
+{
   /* name */
 
   val NAME = "name"
@@ -25,7 +26,8 @@
   val FILE = "file"
   val ID = "id"
 
-  val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
+  val POSITION_PROPERTIES =
+    Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
 
   val POSITION = "position"
   val LOCATION = "location"
diff -r 696d64ed85da -r 375db037f4d2 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sat Aug 29 12:01:25 2009 +0200
+++ b/src/Pure/General/position.scala	Sat Aug 29 14:31:39 2009 +0200
@@ -6,11 +6,9 @@
 
 package isabelle
 
-import java.util.Properties
 
-
-object Position {
-
+object Position
+{
   type T = List[(String, String)]
 
   private def get_string(name: String, pos: T): Option[String] =
@@ -41,5 +39,4 @@
     val end = end_offset_of(pos)
     (begin, if (end.isDefined) end else begin.map(_ + 1))
   }
-
 }
diff -r 696d64ed85da -r 375db037f4d2 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sat Aug 29 12:01:25 2009 +0200
+++ b/src/Pure/General/scan.scala	Sat Aug 29 14:31:39 2009 +0200
@@ -11,7 +11,6 @@
 
 object Scan
 {
-
   /** Lexicon -- position tree **/
 
   object Lexicon
diff -r 696d64ed85da -r 375db037f4d2 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Sat Aug 29 12:01:25 2009 +0200
+++ b/src/Pure/General/yxml.scala	Sat Aug 29 14:31:39 2009 +0200
@@ -7,8 +7,8 @@
 package isabelle
 
 
-object YXML {
-
+object YXML
+{
   /* chunk markers */
 
   private val X = '\5'
@@ -22,7 +22,8 @@
   private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] {
     private val end = source.length
     private var state = if (end == 0) None else get_chunk(-1)
-    private def get_chunk(i: Int) = {
+    private def get_chunk(i: Int) =
+    {
       if (i < end) {
         var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
         Some((source.subSequence(i + 1, j), j))
@@ -55,8 +56,8 @@
   }
 
 
-  def parse_body(source: CharSequence) = {
-
+  def parse_body(source: CharSequence): List[XML.Tree] =
+  {
     /* stack operations */
 
     var stack: List[((String, XML.Attributes), List[XML.Tree])] = null
@@ -94,7 +95,7 @@
     }
   }
 
-  def parse(source: CharSequence) =
+  def parse(source: CharSequence): XML.Tree =
     parse_body(source) match {
       case List(result) => result
       case Nil => XML.Text("")
@@ -108,14 +109,15 @@
     XML.Elem (Markup.BAD, Nil,
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
-  def parse_body_failsafe(source: CharSequence) = {
+  def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
+  {
     try { parse_body(source) }
     catch { case _: RuntimeException => List(markup_failsafe(source)) }
   }
 
-  def parse_failsafe(source: CharSequence) = {
+  def parse_failsafe(source: CharSequence): XML.Tree =
+  {
     try { parse(source) }
     catch { case _: RuntimeException => markup_failsafe(source) }
   }
-
 }
diff -r 696d64ed85da -r 375db037f4d2 src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Sat Aug 29 12:01:25 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala	Sat Aug 29 14:31:39 2009 +0200
@@ -6,7 +6,9 @@
 
 package isabelle
 
-object IsarDocument {
+
+object IsarDocument
+{
   /* unique identifiers */
 
   type State_ID = String
@@ -14,6 +16,7 @@
   type Document_ID = String
 }
 
+
 trait IsarDocument extends Isabelle_Process
 {
   import IsarDocument._
diff -r 696d64ed85da -r 375db037f4d2 src/Pure/Isar/outer_keyword.scala
--- a/src/Pure/Isar/outer_keyword.scala	Sat Aug 29 12:01:25 2009 +0200
+++ b/src/Pure/Isar/outer_keyword.scala	Sat Aug 29 14:31:39 2009 +0200
@@ -6,8 +6,9 @@
 
 package isabelle
 
-object OuterKeyword {
 
+object OuterKeyword
+{
   val MINOR = "minor"
   val CONTROL = "control"
   val DIAG = "diag"
diff -r 696d64ed85da -r 375db037f4d2 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Aug 29 12:01:25 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Aug 29 14:31:39 2009 +0200
@@ -42,13 +42,11 @@
     val rc = proc.waitFor
     (output, rc)
   }
-
 }
 
 
 class Isabelle_System
 {
-
   /** unique ids **/
 
   private var id_count: BigInt = 0
@@ -244,6 +242,7 @@
   }
 
 
+
   /** system tools **/
 
   /* external processes */
@@ -296,6 +295,7 @@
   }
 
 
+
   /** Isabelle resources **/
 
   /* components */
diff -r 696d64ed85da -r 375db037f4d2 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sat Aug 29 12:01:25 2009 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sat Aug 29 14:31:39 2009 +0200
@@ -6,8 +6,9 @@
 
 package isabelle
 
-object ThyHeader {
 
+object ThyHeader
+{
   val HEADER = "header"
   val THEORY = "theory"
   val IMPORTS = "imports"