--- a/src/Pure/Concurrent/future.scala Tue Jan 05 15:35:01 2010 +0100
+++ b/src/Pure/Concurrent/future.scala Tue Jan 05 16:51:01 2010 +0100
@@ -41,7 +41,8 @@
abstract class Promise[A] extends Future[A]
{
- def fulfill(x: A): Unit
+ def fulfill_result(res: Exn.Result[A]): Unit
+ def fulfill(x: A) { fulfill_result(Exn.Res(x)) }
}
private class Finished_Future[A](x: A) extends Future[A]
@@ -72,32 +73,34 @@
private class Promise_Future[A] extends Promise[A]
{
- @volatile private var result: Option[A] = None
+ @volatile private var result: Option[Exn.Result[A]] = None
private case object Read
- private case class Write(x: A)
+ private case class Write(res: Exn.Result[A])
private val receiver = actor {
loop {
react {
case Read if result.isDefined => reply(result.get)
- case Write(x) =>
+ case Write(res) =>
if (result.isDefined) reply(false)
- else { result = Some(x); reply(true) }
+ else { result = Some(res); reply(true) }
}
}
}
- def peek: Option[Exn.Result[A]] = result.map(Exn.Res(_))
+ def peek: Option[Exn.Result[A]] = result
def join: A =
- result match {
- case Some(res) => res
- case None => (receiver !? Read).asInstanceOf[A]
+ Exn.release {
+ result match {
+ case Some(res) => res
+ case None => (receiver !? Read).asInstanceOf[Exn.Result[A]]
+ }
}
- def fulfill(x: A) {
- receiver !? Write(x) match {
+ def fulfill_result(res: Exn.Result[A]) {
+ receiver !? Write(res) match {
case false => error("Duplicate fulfillment of promise")
case _ =>
}
--- a/src/Pure/General/scan.scala Tue Jan 05 15:35:01 2010 +0100
+++ b/src/Pure/General/scan.scala Tue Jan 05 16:51:01 2010 +0100
@@ -220,8 +220,8 @@
val comment_text =
rep(many1(sym => sym != "*" && sym != "(" && Symbol.is_closed(sym)) |
"""\*(?!\))|\((?!\*)""".r)
- val comment_open = "(*" ~ comment_text ^^ (_ => ())
- val comment_close = comment_text ~ "*)" ^^ (_ => ())
+ val comment_open = "(*" ~ comment_text ^^^ ()
+ val comment_close = comment_text ~ "*)" ^^^ ()
def apply(in: Input) =
{
@@ -283,17 +283,20 @@
val string = quoted("\"") ^^ (x => Token(Token_Kind.STRING, x))
val alt_string = quoted("`") ^^ (x => Token(Token_Kind.ALT_STRING, x))
- val bad_input = many1(sym => !(symbols.is_blank(sym))) ^^
- (x => Token(Token_Kind.BAD_INPUT, x))
+ val junk = many1(sym => !(symbols.is_blank(sym)))
+ val bad_delimiter =
+ ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token_Kind.BAD_INPUT, x + y) }
+ val bad = junk ^^ (x => Token(Token_Kind.BAD_INPUT, x))
/* tokens */
(space | (string | (alt_string | (verbatim ^^ (x => Token(Token_Kind.VERBATIM, x)) |
comment ^^ (x => Token(Token_Kind.COMMENT, x)))))) |
+ bad_delimiter |
((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
keyword ^^ (x => Token(if (is_command(x)) Token_Kind.COMMAND else Token_Kind.KEYWORD, x))) |
- bad_input
+ bad
}
}
--- a/src/Pure/IsaMakefile Tue Jan 05 15:35:01 2010 +0100
+++ b/src/Pure/IsaMakefile Tue Jan 05 16:51:01 2010 +0100
@@ -132,7 +132,7 @@
System/isabelle_system.scala System/platform.scala \
System/session_manager.scala System/standard_system.scala \
Thy/completion.scala Thy/html.scala Thy/thy_header.scala \
- library.scala
+ Thy/thy_syntax.scala library.scala
JAR_DIR = $(ISABELLE_HOME)/lib/classes
PURE_JAR = $(JAR_DIR)/Pure.jar
--- a/src/Pure/Isar/outer_lex.scala Tue Jan 05 15:35:01 2010 +0100
+++ b/src/Pure/Isar/outer_lex.scala Tue Jan 05 16:51:01 2010 +0100
@@ -33,6 +33,7 @@
sealed case class Token(val kind: Token_Kind.Value, val source: String)
{
+ def is_command: Boolean = kind == Token_Kind.COMMAND
def is_delimited: Boolean =
kind == Token_Kind.STRING ||
kind == Token_Kind.ALT_STRING ||
@@ -48,6 +49,7 @@
def is_space: Boolean = kind == Token_Kind.SPACE
def is_comment: Boolean = kind == Token_Kind.COMMENT
def is_proper: Boolean = !(is_space || is_comment)
+ def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
def content: String =
if (kind == Token_Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
--- a/src/Pure/Isar/outer_parse.scala Tue Jan 05 15:35:01 2010 +0100
+++ b/src/Pure/Isar/outer_parse.scala Tue Jan 05 16:51:01 2010 +0100
@@ -17,8 +17,10 @@
{
type Elem = Outer_Lex.Token
+ def filter_proper = true
+
private def proper(in: Input): Input =
- if (in.atEnd || in.first.is_proper) in
+ if (in.atEnd || in.first.is_proper || !filter_proper) in
else proper(in.rest)
def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
@@ -41,11 +43,12 @@
}
}
+ def not_eof: Parser[Elem] = token("input token", _ => true)
+ def eof: Parser[Unit] = not(not_eof)
+
def atom(s: String, pred: Elem => Boolean): Parser[String] =
token(s, pred) ^^ (_.content)
- def not_eof: Parser[Elem] = token("input token", _ => true)
-
def keyword(name: String): Parser[String] =
atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
--- a/src/Pure/Isar/outer_syntax.scala Tue Jan 05 15:35:01 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Tue Jan 05 16:51:01 2010 +0100
@@ -45,7 +45,7 @@
parseAll(rep(token(symbols, is_command)), input) match {
case Success(tokens, _) => tokens
- case _ => error("Failed to tokenize input:\n" + input.source.toString)
+ case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_syntax.scala Tue Jan 05 16:51:01 2010 +0100
@@ -0,0 +1,36 @@
+/* Title: Pure/Thy/thy_syntax.scala
+ Author: Makarius
+
+Superficial theory syntax: command spans.
+*/
+
+package isabelle
+
+
+class Thy_Syntax
+{
+ private val parser = new Outer_Parse.Parser
+ {
+ override def filter_proper = false
+
+ val command_span: Parser[Span] =
+ {
+ val whitespace = token("white space", tok => tok.is_space || tok.is_comment)
+ val command = token("command keyword", _.is_command)
+ val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
+ command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
+ }
+ }
+
+ type Span = List[Outer_Lex.Token]
+
+ def parse_spans(toks: List[Outer_Lex.Token]): List[Span] =
+ {
+ import parser._
+
+ parse(rep(command_span), Outer_Lex.reader(toks)) match {
+ case Success(spans, rest) if rest.atEnd => spans
+ case bad => error(bad.toString)
+ }
+ }
+}