# HG changeset patch
# User wenzelm
# Date 1262706661 -3600
# Node ID 2cb69632d3fa3a101a97df72069c77ec157e0043
# Parent  5b3958210c35d228fe7773db4e509cc8b4ed43ac# Parent  b149b70832361d9a20a677d55c672de321cbc993
merged

diff -r 5b3958210c35 -r 2cb69632d3fa src/Pure/Concurrent/future.scala
--- 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 _ =>
     }
diff -r 5b3958210c35 -r 2cb69632d3fa src/Pure/General/scan.scala
--- 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
     }
   }
 
diff -r 5b3958210c35 -r 2cb69632d3fa src/Pure/IsaMakefile
--- 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
diff -r 5b3958210c35 -r 2cb69632d3fa src/Pure/Isar/outer_lex.scala
--- 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)
diff -r 5b3958210c35 -r 2cb69632d3fa src/Pure/Isar/outer_parse.scala
--- 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)
diff -r 5b3958210c35 -r 2cb69632d3fa src/Pure/Isar/outer_syntax.scala
--- 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)
     }
   }
 
diff -r 5b3958210c35 -r 2cb69632d3fa src/Pure/Thy/thy_syntax.scala
--- /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)
+    }
+  }
+}