1.1 --- a/src/Pure/General/markup.scala Sat Aug 29 12:01:25 2009 +0200
1.2 +++ b/src/Pure/General/markup.scala Sat Aug 29 14:31:39 2009 +0200
1.3 @@ -6,8 +6,9 @@
1.4
1.5 package isabelle
1.6
1.7 -object Markup {
1.8
1.9 +object Markup
1.10 +{
1.11 /* name */
1.12
1.13 val NAME = "name"
1.14 @@ -25,7 +26,8 @@
1.15 val FILE = "file"
1.16 val ID = "id"
1.17
1.18 - val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
1.19 + val POSITION_PROPERTIES =
1.20 + Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
1.21
1.22 val POSITION = "position"
1.23 val LOCATION = "location"
2.1 --- a/src/Pure/General/position.scala Sat Aug 29 12:01:25 2009 +0200
2.2 +++ b/src/Pure/General/position.scala Sat Aug 29 14:31:39 2009 +0200
2.3 @@ -6,11 +6,9 @@
2.4
2.5 package isabelle
2.6
2.7 -import java.util.Properties
2.8
2.9 -
2.10 -object Position {
2.11 -
2.12 +object Position
2.13 +{
2.14 type T = List[(String, String)]
2.15
2.16 private def get_string(name: String, pos: T): Option[String] =
2.17 @@ -41,5 +39,4 @@
2.18 val end = end_offset_of(pos)
2.19 (begin, if (end.isDefined) end else begin.map(_ + 1))
2.20 }
2.21 -
2.22 }
3.1 --- a/src/Pure/General/scan.scala Sat Aug 29 12:01:25 2009 +0200
3.2 +++ b/src/Pure/General/scan.scala Sat Aug 29 14:31:39 2009 +0200
3.3 @@ -11,7 +11,6 @@
3.4
3.5 object Scan
3.6 {
3.7 -
3.8 /** Lexicon -- position tree **/
3.9
3.10 object Lexicon
4.1 --- a/src/Pure/General/yxml.scala Sat Aug 29 12:01:25 2009 +0200
4.2 +++ b/src/Pure/General/yxml.scala Sat Aug 29 14:31:39 2009 +0200
4.3 @@ -7,8 +7,8 @@
4.4 package isabelle
4.5
4.6
4.7 -object YXML {
4.8 -
4.9 +object YXML
4.10 +{
4.11 /* chunk markers */
4.12
4.13 private val X = '\5'
4.14 @@ -22,7 +22,8 @@
4.15 private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] {
4.16 private val end = source.length
4.17 private var state = if (end == 0) None else get_chunk(-1)
4.18 - private def get_chunk(i: Int) = {
4.19 + private def get_chunk(i: Int) =
4.20 + {
4.21 if (i < end) {
4.22 var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
4.23 Some((source.subSequence(i + 1, j), j))
4.24 @@ -55,8 +56,8 @@
4.25 }
4.26
4.27
4.28 - def parse_body(source: CharSequence) = {
4.29 -
4.30 + def parse_body(source: CharSequence): List[XML.Tree] =
4.31 + {
4.32 /* stack operations */
4.33
4.34 var stack: List[((String, XML.Attributes), List[XML.Tree])] = null
4.35 @@ -94,7 +95,7 @@
4.36 }
4.37 }
4.38
4.39 - def parse(source: CharSequence) =
4.40 + def parse(source: CharSequence): XML.Tree =
4.41 parse_body(source) match {
4.42 case List(result) => result
4.43 case Nil => XML.Text("")
4.44 @@ -108,14 +109,15 @@
4.45 XML.Elem (Markup.BAD, Nil,
4.46 List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
4.47
4.48 - def parse_body_failsafe(source: CharSequence) = {
4.49 + def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
4.50 + {
4.51 try { parse_body(source) }
4.52 catch { case _: RuntimeException => List(markup_failsafe(source)) }
4.53 }
4.54
4.55 - def parse_failsafe(source: CharSequence) = {
4.56 + def parse_failsafe(source: CharSequence): XML.Tree =
4.57 + {
4.58 try { parse(source) }
4.59 catch { case _: RuntimeException => markup_failsafe(source) }
4.60 }
4.61 -
4.62 }
5.1 --- a/src/Pure/Isar/isar_document.scala Sat Aug 29 12:01:25 2009 +0200
5.2 +++ b/src/Pure/Isar/isar_document.scala Sat Aug 29 14:31:39 2009 +0200
5.3 @@ -6,7 +6,9 @@
5.4
5.5 package isabelle
5.6
5.7 -object IsarDocument {
5.8 +
5.9 +object IsarDocument
5.10 +{
5.11 /* unique identifiers */
5.12
5.13 type State_ID = String
5.14 @@ -14,6 +16,7 @@
5.15 type Document_ID = String
5.16 }
5.17
5.18 +
5.19 trait IsarDocument extends Isabelle_Process
5.20 {
5.21 import IsarDocument._
6.1 --- a/src/Pure/Isar/outer_keyword.scala Sat Aug 29 12:01:25 2009 +0200
6.2 +++ b/src/Pure/Isar/outer_keyword.scala Sat Aug 29 14:31:39 2009 +0200
6.3 @@ -6,8 +6,9 @@
6.4
6.5 package isabelle
6.6
6.7 -object OuterKeyword {
6.8
6.9 +object OuterKeyword
6.10 +{
6.11 val MINOR = "minor"
6.12 val CONTROL = "control"
6.13 val DIAG = "diag"
7.1 --- a/src/Pure/System/isabelle_system.scala Sat Aug 29 12:01:25 2009 +0200
7.2 +++ b/src/Pure/System/isabelle_system.scala Sat Aug 29 14:31:39 2009 +0200
7.3 @@ -42,13 +42,11 @@
7.4 val rc = proc.waitFor
7.5 (output, rc)
7.6 }
7.7 -
7.8 }
7.9
7.10
7.11 class Isabelle_System
7.12 {
7.13 -
7.14 /** unique ids **/
7.15
7.16 private var id_count: BigInt = 0
7.17 @@ -244,6 +242,7 @@
7.18 }
7.19
7.20
7.21 +
7.22 /** system tools **/
7.23
7.24 /* external processes */
7.25 @@ -296,6 +295,7 @@
7.26 }
7.27
7.28
7.29 +
7.30 /** Isabelle resources **/
7.31
7.32 /* components */
8.1 --- a/src/Pure/Thy/thy_header.scala Sat Aug 29 12:01:25 2009 +0200
8.2 +++ b/src/Pure/Thy/thy_header.scala Sat Aug 29 14:31:39 2009 +0200
8.3 @@ -6,8 +6,9 @@
8.4
8.5 package isabelle
8.6
8.7 -object ThyHeader {
8.8
8.9 +object ThyHeader
8.10 +{
8.11 val HEADER = "header"
8.12 val THEORY = "theory"
8.13 val IMPORTS = "imports"