# HG changeset patch
# User boehmes
# Date 1289775325 -3600
# Node ID b6f1da38fa24b94147b095f513b1a0be3c657d5a
# Parent  b8482ff0bc922286a5be06bb2960c30400dbbeee# Parent  9e196062bf889b2d9e4fc00ac6126534e66ae052
merged

diff -r b8482ff0bc92 -r b6f1da38fa24 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Fri Nov 12 17:28:43 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sun Nov 14 23:55:25 2010 +0100
@@ -1476,7 +1476,13 @@
   mutability.  Existing operations @{ML "!"}  and @{ML "op :="} are
   unchanged, but should be used with special precautions, say in a
   strictly local situation that is guaranteed to be restricted to
-  sequential evaluation --- now and in the future.  *}
+  sequential evaluation --- now and in the future.
+
+  \begin{warn}
+  Never @{ML_text "open Unsynchronized"}, not even in a local scope!
+  Pretending that mutable state is no problem is a very bad idea.
+  \end{warn}
+*}
 
 
 section {* Thread-safe programming \label{sec:multi-threading} *}
diff -r b8482ff0bc92 -r b6f1da38fa24 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Nov 12 17:28:43 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Sun Nov 14 23:55:25 2010 +0100
@@ -1965,7 +1965,12 @@
   mutability.  Existing operations \verb|!|  and \verb|op :=| are
   unchanged, but should be used with special precautions, say in a
   strictly local situation that is guaranteed to be restricted to
-  sequential evaluation --- now and in the future.%
+  sequential evaluation --- now and in the future.
+
+  \begin{warn}
+  Never \verb|open Unsynchronized|, not even in a local scope!
+  Pretending that mutable state is no problem is a very bad idea.
+  \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r b8482ff0bc92 -r b6f1da38fa24 src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/HOL/Import/import_syntax.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -147,7 +147,7 @@
         val inp = TextIO.inputAll is
         val _ = TextIO.closeIn is
         val orig_source = Source.of_string inp
-        val symb_source = Symbol.source {do_recover = false} orig_source
+        val symb_source = Symbol.source orig_source
         val lexes =
           (Scan.make_lexicon
             (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
diff -r b8482ff0bc92 -r b6f1da38fa24 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -389,7 +389,7 @@
     val get = maps (ProofContext.get_fact ctxt o fst)
   in
     Source.of_string name
-    |> Symbol.source {do_recover=false}
+    |> Symbol.source
     |> Token.source {do_recover=SOME false} lex Position.start
     |> Token.source_proper
     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/General/scan.scala	Sun Nov 14 23:55:25 2010 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/scan.scala
     Author:     Makarius
 
-Efficient scanning of keywords.
+Efficient scanning of keywords and tokens.
 */
 
 package isabelle
@@ -181,8 +181,7 @@
     private def quoted(quote: String): Parser[String] =
     {
       quote ~
-        rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_wellformed(sym)) |
-          "\\" + quote | "\\\\" |
+        rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
           (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ~
       quote ^^ { case x ~ ys ~ z => x + ys.mkString + z }
     }.named("quoted")
@@ -193,7 +192,7 @@
       val body = source.substring(1, source.length - 1)
       if (body.exists(_ == '\\')) {
         val content =
-          rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_wellformed(sym)) |
+          rep(many1(sym => sym != quote && sym != "\\") |
               "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString }))
         parseAll(content ^^ (_.mkString), body).get
       }
@@ -205,7 +204,7 @@
 
     private def verbatim: Parser[String] =
     {
-      "{*" ~ rep(many1(sym => sym != "*" && Symbol.is_wellformed(sym)) | """\*(?!\})""".r) ~ "*}" ^^
+      "{*" ~ rep(many1(sym => sym != "*") | """\*(?!\})""".r) ~ "*}" ^^
         { case x ~ ys ~ z => x + ys.mkString + z }
     }.named("verbatim")
 
@@ -221,8 +220,7 @@
     def comment: Parser[String] = new Parser[String]
     {
       val comment_text =
-        rep(many1(sym => sym != "*" && sym != "(" && Symbol.is_wellformed(sym)) |
-          """\*(?!\))|\((?!\*)""".r)
+        rep(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
       val comment_open = "(*" ~ comment_text ^^^ ()
       val comment_close = comment_text ~ "*)" ^^^ ()
 
@@ -277,8 +275,7 @@
         ("-" ~ natdot ^^ { case x ~ y => x + y } | natdot) ^^ (x => Token(Token.Kind.FLOAT, x))
 
       val sym_ident =
-        (many1(symbols.is_symbolic_char) |
-          one(sym => symbols.is_symbolic(sym) & Symbol.is_wellformed(sym))) ^^
+        (many1(symbols.is_symbolic_char) | one(sym => symbols.is_symbolic(sym))) ^^
         (x => Token(Token.Kind.SYM_IDENT, x))
 
       val space = many1(symbols.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/General/symbol.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -6,7 +6,7 @@
 
 signature SYMBOL =
 sig
-  type symbol
+  type symbol = string
   val SOH: symbol
   val STX: symbol
   val ENQ: symbol
@@ -24,10 +24,9 @@
   val stopper: symbol Scan.stopper
   val sync: symbol
   val is_sync: symbol -> bool
-  val malformed: symbol
-  val end_malformed: symbol
-  val separate_chars: string -> string
   val is_regular: symbol -> bool
+  val is_malformed: symbol -> bool
+  val malformed_msg: symbol -> string
   val is_ascii: symbol -> bool
   val is_ascii_letter: symbol -> bool
   val is_ascii_digit: symbol -> bool
@@ -42,7 +41,9 @@
   val is_raw: symbol -> bool
   val decode_raw: symbol -> string
   val encode_raw: string -> string
-  datatype sym = Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string
+  datatype sym =
+    Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string |
+    Malformed of string
   val decode: symbol -> sym
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
@@ -56,8 +57,7 @@
   val beginning: int -> symbol list -> string
   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
   val scan_id: string list -> string * string list
-  val source: {do_recover: bool} -> (string, 'a) Source.source ->
-    (symbol, (string, 'a) Source.source) Source.source
+  val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
   val esc: symbol -> string
   val escape: string -> string
@@ -111,11 +111,11 @@
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
 
 fun is_symbolic s =
-  String.isPrefix "\\<" s andalso not (String.isPrefix "\\<^" s);
+  String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
 
 fun is_printable s =
   if is_char s then ord space <= ord s andalso ord s <= ord "~"
-  else is_utf8 s orelse not (String.isPrefix "\\<^" s);
+  else is_utf8 s orelse is_symbolic s;
 
 
 (* input source control *)
@@ -128,14 +128,10 @@
 val sync = "\\<^sync>";
 fun is_sync s = s = sync;
 
-val malformed = "[[";
-val end_malformed = "]]";
+fun is_regular s = not_eof s andalso s <> sync;
 
-val separate_chars = explode #> space_implode space;
-fun malformed_msg s = "Malformed symbolic character: " ^ quote (separate_chars s);
-
-fun is_regular s =
-  not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
+fun is_malformed s = String.isPrefix "\\<" s andalso not (String.isSuffix ">" s);
+fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
 
 
 (* ascii symbols *)
@@ -225,15 +221,16 @@
 (* symbol variants *)
 
 datatype sym =
-  Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string;
+  Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string |
+  Malformed of string;
 
 fun decode s =
   if is_char s then Char s
   else if is_utf8 s then UTF8 s
   else if is_raw s then Raw (decode_raw s)
+  else if is_malformed s then Malformed s
   else if String.isPrefix "\\<^" s then Ctrl (String.substring (s, 3, size s - 4))
-  else if String.isPrefix "\\<" s then Sym (String.substring (s, 2, size s - 3))
-  else error (malformed_msg s);
+  else Sym (String.substring (s, 2, size s - 3));
 
 
 (* standard symbol kinds *)
@@ -445,30 +442,18 @@
   Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
   Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
 
-val scan =
+val scan_total =
   Scan.one is_plain ||
   Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
   scan_encoded_newline ||
-  ($$ "\\" ^^ $$ "<" ^^
-    !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))
-      (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
+  ($$ "\\" ^^ $$ "<" ^^ (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
+  Scan.this_string "\\<^" ||
+  Scan.this_string "\\<" ||
   Scan.one not_eof;
 
-val scan_resync =
-  Scan.one is_ascii_blank || $$ "\"" || $$ "`" || $$ "\\" ||
-  Scan.this_string "(*" || Scan.this_string "*)" ||
-  Scan.this_string "{*" || Scan.this_string "*}";
-
-val recover =
-  Scan.this ["\\", "<"] @@@
-    Scan.repeat (Scan.unless scan_resync (Scan.one not_eof))
-  >> (fn ss => malformed :: ss @ [end_malformed]);
-
 in
 
-fun source {do_recover} src =
-  Source.source stopper (Scan.bulk scan)
-    (if do_recover then SOME (false, K recover) else NONE) src;
+fun source src = Source.source stopper (Scan.bulk scan_total) NONE src;
 
 end;
 
@@ -487,7 +472,7 @@
 fun sym_explode str =
   let val chs = explode str in
     if no_explode chs then chs
-    else Source.exhaust (source {do_recover = false} (Source.of_list chs))
+    else Source.exhaust (source (Source.of_list chs))
   end;
 
 end;
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/General/symbol.scala	Sun Nov 14 23:55:25 2010 +0100
@@ -31,22 +31,20 @@
   /* Symbol regexps */
 
   private val plain = new Regex("""(?xs)
-      [^\r\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+      [^\r\\\ud800-\udfff\ufffd] | [\ud800-\udbff][\udc00-\udfff] """)
 
-  private val newline = new Regex("""(?xs) \r\n | \r """)
+  private val physical_newline = new Regex("""(?xs) \n | \r\n | \r """)
 
   private val symbol = new Regex("""(?xs)
       \\ < (?:
       \^? [A-Za-z][A-Za-z0-9_']* |
       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
 
-  // FIXME cover bad surrogates!?
-  // FIXME check wrt. Isabelle/ML version
-  private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
-    """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
+  private val malformed_symbol = new Regex("(?xs) (?!" + symbol + ")" +
+    """ [\ud800-\udbff\ufffd] | \\<\^? """)
 
-  // total pattern
-  val regex = new Regex(plain + "|" + newline + "|" + symbol + "|" + bad_symbol + "| .")
+  val regex_total =
+    new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + malformed_symbol + "| .")
 
 
   /* basic matching */
@@ -56,12 +54,12 @@
   def is_physical_newline(s: CharSequence): Boolean =
     "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
 
-  def is_wellformed(s: CharSequence): Boolean =
-    s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
+  def is_malformed(s: CharSequence): Boolean =
+    !(s.length == 1 && is_plain(s.charAt(0))) && malformed_symbol.pattern.matcher(s).matches
 
   class Matcher(text: CharSequence)
   {
-    private val matcher = regex.pattern.matcher(text)
+    private val matcher = regex_total.pattern.matcher(text)
     def apply(start: Int, end: Int): Int =
     {
       require(0 <= start && start < end && end <= text.length)
@@ -81,7 +79,8 @@
     private val matcher = new Matcher(text)
     private var i = 0
     def hasNext = i < text.length
-    def next = {
+    def next =
+    {
       val n = matcher(i, text.length)
       val s = text.subSequence(i, i + n)
       i += n
@@ -161,7 +160,7 @@
     def recode(text: String): String =
     {
       val len = text.length
-      val matcher = regex.pattern.matcher(text)
+      val matcher = regex_total.pattern.matcher(text)
       val result = new StringBuilder(len)
       var i = 0
       while (i < len) {
@@ -203,7 +202,7 @@
         }
       }
       decl.split("\\s+").toList match {
-        case sym :: props if sym.length > 1 && is_wellformed(sym) => (sym, read_props(props))
+        case sym :: props if sym.length > 1 && !is_malformed(sym) => (sym, read_props(props))
         case _ => err()
       }
     }
@@ -312,6 +311,7 @@
     def is_letdig(sym: String): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
     def is_blank(sym: String): Boolean = blanks.contains(sym)
     def is_symbolic_char(sym: String): Boolean = sym_chars.contains(sym)
-    def is_symbolic(sym: String): Boolean = sym.startsWith("\\<") && !sym.startsWith("\\<^")
+    def is_symbolic(sym: String): Boolean =
+      sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
   }
 }
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -182,7 +182,6 @@
 
 structure Basic_Symbol_Pos =   (*not open by default*)
 struct
-  val symbol = Symbol_Pos.symbol;
   val $$$ = Symbol_Pos.$$$;
   val ~$$$ = Symbol_Pos.~$$$;
 end;
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -187,13 +187,13 @@
 
 fun scan pos str =
   Source.of_string str
-  |> Symbol.source {do_recover = false}
+  |> Symbol.source
   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   |> Source.exhaust;
 
 fun parse pos str =
   Source.of_string str
-  |> Symbol.source {do_recover = false}
+  |> Symbol.source
   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   |> toplevel_source false NONE get_command
   |> Source.exhaust;
@@ -224,7 +224,7 @@
 
 fun isar in_stream term : isar =
   Source.tty in_stream
-  |> Symbol.source {do_recover = true}
+  |> Symbol.source
   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) get_command;
 
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Sun Nov 14 23:55:25 2010 +0100
@@ -18,11 +18,11 @@
 
   def keyword_kind(name: String): Option[String] = keywords.get(name)
 
-  def + (name: String, kind: String): Outer_Syntax =
+  def + (name: String, kind: String, replace: String): Outer_Syntax =
   {
     val new_keywords = keywords + (name -> kind)
     val new_lexicon = lexicon + name
-    val new_completion = completion + name
+    val new_completion = completion + (name, replace)
     new Outer_Syntax(symbols) {
       override val lexicon = new_lexicon
       override val keywords = new_keywords
@@ -30,6 +30,8 @@
     }
   }
 
+  def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
+
   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
 
   def is_command(name: String): Boolean =
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/Isar/token.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -200,7 +200,6 @@
   | AltString => x |> enclose "`" "`" o escape "`"
   | Verbatim => x |> enclose "{*" "*}"
   | Comment => x |> enclose "(*" "*)"
-  | Malformed => space_implode " " (explode x)
   | Sync => ""
   | EOF => ""
   | _ => x);
@@ -210,8 +209,7 @@
   else
     let
       val k = str_of_kind (kind_of tok);
-      val s = unparse tok
-        handle ERROR _ => Symbol.separate_chars (content_of tok);
+      val s = unparse tok;
     in
       if s = "" then (k, "")
       else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
@@ -270,8 +268,8 @@
 val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
 
 val scan_symid =
-  Scan.many1 (is_sym_char o symbol) ||
-  Scan.one (Symbol.is_symbolic o symbol) >> single;
+  Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
+  Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
 
 fun is_symid str =
   (case try Symbol.explode str of
@@ -302,8 +300,8 @@
 fun is_space s = Symbol.is_blank s andalso s <> "\n";
 
 val scan_space =
-  Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
-  Scan.many (is_space o symbol) @@@ $$$ "\n";
+  Scan.many1 (is_space o Symbol_Pos.symbol) @@@ Scan.optional ($$$ "\n") [] ||
+  Scan.many (is_space o Symbol_Pos.symbol) @@@ $$$ "\n";
 
 
 (* scan comment *)
@@ -312,14 +310,6 @@
   Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
 
 
-(* scan malformed symbols *)
-
-val scan_malformed =
-  $$$ Symbol.malformed |--
-    Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
-  --| Scan.option ($$$ Symbol.end_malformed);
-
-
 
 (** token sources **)
 
@@ -341,8 +331,8 @@
     scan_verbatim >> token_range Verbatim ||
     scan_comment >> token_range Comment ||
     scan_space >> token Space ||
-    scan_malformed >> token Malformed ||
-    Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
+    Scan.one (Symbol.is_malformed o Symbol_Pos.symbol) >> (token Malformed o single) ||
+    Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
     (Scan.max token_leq
       (Scan.max token_leq
         (Scan.literal lex2 >> pair Command)
@@ -357,7 +347,7 @@
         scan_symid >> pair SymIdent) >> uncurry token));
 
 fun recover msg =
-  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
+  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o Symbol_Pos.symbol)
   >> (single o token (Error msg));
 
 in
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -135,7 +135,7 @@
 
 (* blanks *)
 
-val scan_blank = Scan.one (Symbol.is_ascii_blank o symbol);
+val scan_blank = Scan.one (Symbol.is_ascii_blank o Symbol_Pos.symbol);
 val scan_blanks1 = Scan.repeat1 scan_blank;
 
 
@@ -158,11 +158,15 @@
 local
 
 val scan_letdigs =
-  Scan.many ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o symbol);
+  Scan.many
+    ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o
+      Symbol_Pos.symbol);
 
-val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o symbol) -- scan_letdigs >> op ::;
+val scan_alphanumeric =
+  Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;
 
-val scan_symbolic = Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o symbol);
+val scan_symbolic =
+  Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
 
 in
 
@@ -180,8 +184,8 @@
 
 local
 
-val scan_dec = Scan.many1 (Symbol.is_ascii_digit o symbol);
-val scan_hex = Scan.many1 (Symbol.is_ascii_hex o symbol);
+val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol);
+val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_sign = Scan.optional ($$$ "~") [];
 val scan_decint = scan_sign @@@ scan_dec;
 
@@ -207,11 +211,11 @@
 local
 
 val scan_escape =
-  Scan.one (member (op =) (explode "\"\\abtnvfr") o symbol) >> single ||
+  Scan.one (member (op =) (explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
   $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
-  Scan.one (Symbol.is_ascii_digit o symbol) --
-    Scan.one (Symbol.is_ascii_digit o symbol) --
-    Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]);
+  Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
+    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
+    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
 
 val scan_str =
   Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
@@ -256,7 +260,7 @@
 val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
 
 fun recover msg =
-  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
+  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o Symbol_Pos.symbol)
   >> (fn cs => [token (Error msg) cs]);
 
 in
@@ -265,11 +269,7 @@
   Symbol_Pos.source (Position.line 1) src
   |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
 
-val tokenize =
-  Source.of_string #>
-  Symbol.source {do_recover = true} #>
-  source #>
-  Source.exhaust;
+val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
 
 fun read pos txt =
   let
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/PIDE/document.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -197,13 +197,11 @@
   | NONE => ());
 
 fun async_state tr st =
-  if Toplevel.print_of tr then
-    ignore
-      (Future.fork_group (Task_Queue.new_group NONE)
-        (fn () =>
-          Toplevel.setmp_thread_position tr
-            (fn () => Toplevel.print_state false st) ()))
-  else ();
+  ignore
+    (Future.fork_group (Task_Queue.new_group NONE)
+      (fn () =>
+        Toplevel.setmp_thread_position tr
+          (fn () => Toplevel.print_state false st) ()));
 
 fun run int tr st =
   (case Toplevel.transition int tr st of
@@ -223,9 +221,12 @@
       | NONE => Exn.Result ()) of
     Exn.Result () =>
       let
-        val int = is_some (Toplevel.init_of tr);
+        val is_init = is_some (Toplevel.init_of tr);
+        val is_proof = Keyword.is_proof (Toplevel.name_of tr);
+        val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
+
         val start = start_timing ();
-        val (errs, result) = run int tr st;
+        val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
         val _ = timing tr (end_timing start);
         val _ = List.app (Toplevel.error_msg tr) errs;
         val res =
@@ -234,7 +235,7 @@
           | SOME st' =>
              (Toplevel.status tr Markup.finished;
               proof_status tr st';
-              if int then () else async_state tr st';
+              if do_print then async_state tr st' else ();
               (true, st')));
       in res end
   | Exn.Exn exn =>
@@ -319,8 +320,7 @@
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
       val _ = List.app Future.cancel execution;
-      fun await_cancellation () =
-        uninterruptible (fn _ => fn () => Future.join_results execution) ();
+      fun await_cancellation () = Future.join_results execution;
 
       val execution' = (* FIXME proper node deps *)
         node_names_of version |> map (fn name =>
@@ -328,6 +328,9 @@
             (await_cancellation ();
               fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
                 (get_node version name) ())));
+
+      val _ = await_cancellation ();
+
     in (versions, commands, execs, execution') end);
 
 end;
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -103,15 +103,18 @@
 
 fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
 
-val scan_id = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
+val scan_id =
+  Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::
+  Scan.many (Symbol.is_letdig o Symbol_Pos.symbol);
+
 val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
 val scan_tid = $$$ "'" @@@ scan_id;
 
-val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
+val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
 val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
 val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
 val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
-val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o symbol);
+val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
 
 val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
@@ -221,7 +224,9 @@
 
 val scan_chr =
   $$$ "\\" |-- $$$ "'" ||
-  Scan.one ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o symbol) >> single ||
+  Scan.one
+    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
+      Symbol_Pos.symbol) >> single ||
   $$$ "'" --| Scan.ahead (~$$$ "'");
 
 val scan_str =
@@ -237,7 +242,7 @@
 
 fun explode_xstr str =
   (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
-    SOME cs => map symbol cs
+    SOME cs => map Symbol_Pos.symbol cs
   | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
 
 
@@ -271,7 +276,7 @@
       Symbol_Pos.scan_comment !!! >> token Comment ||
       Scan.max token_leq scan_lit scan_val ||
       scan_str >> token StrSy ||
-      Scan.many1 (Symbol.is_blank o symbol) >> token Space;
+      Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
   in
     (case Scan.error
         (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
@@ -301,8 +306,8 @@
           if Symbol.is_digit c then chop_idx cs (c :: ds)
           else idxname (c :: cs) ds;
 
-    val scan = (scan_id >> map symbol) --
-      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map symbol)) ~1;
+    val scan = (scan_id >> map Symbol_Pos.symbol) --
+      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
   in
     scan >>
       (fn (cs, ~1) => chop_idx (rev cs) []
@@ -334,7 +339,7 @@
   let
     val scan =
       $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
-      Scan.many (Symbol.is_regular o symbol) >> (free o implode o map symbol);
+      Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (free o implode o map Symbol_Pos.symbol);
   in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
 
 
@@ -378,7 +383,7 @@
 local
 
 fun nat cs =
-  Option.map (#1 o Library.read_int o map symbol)
+  Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
     (Scan.read Symbol_Pos.stopper scan_nat cs);
 
 in
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -168,7 +168,8 @@
     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
     val _ = Output.raw_stdout Symbol.STX;
 
-    val _ = quick_and_dirty := true;  (* FIXME !? *)
+    val _ = quick_and_dirty := true;
+    val _ = Goal.parallel_proofs := 0;
     val _ = Context.set_thread_data NONE;
     val _ = Unsynchronized.change print_mode
       (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/System/session.scala	Sun Nov 14 23:55:25 2010 +0100
@@ -208,7 +208,12 @@
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message
-            if (result.is_ready) phase = Session.Ready
+            if (result.is_ready) {
+              // FIXME move to ML side
+              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
+              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
+              phase = Session.Ready
+            }
             else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
             else if (result.is_exit) phase = Session.Inactive
           }
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/Thy/completion.scala	Sun Nov 14 23:55:25 2010 +0100
@@ -23,7 +23,7 @@
 
     def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
     def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
-    def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
+    def word: Parser[String] = "[a-zA-Z0-9_']{2,}".r
 
     def read(in: CharSequence): Option[String] =
     {
@@ -49,17 +49,19 @@
 
   /* adding stuff */
 
-  def + (keyword: String): Completion =
+  def + (keyword: String, replace: String): Completion =
   {
     val old = this
     new Completion {
       override val words_lex = old.words_lex + keyword
-      override val words_map = old.words_map + (keyword -> keyword)
+      override val words_map = old.words_map + (keyword -> replace)
       override val abbrevs_lex = old.abbrevs_lex
       override val abbrevs_map = old.abbrevs_map
     }
   }
 
+  def + (keyword: String): Completion = this + (keyword, keyword)
+
   def + (symbols: Symbol.Interpretation): Completion =
   {
     val words =
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -101,7 +101,8 @@
   | Symbol.Ctrl s =>
       if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
       else output_chrs sym
-  | Symbol.Raw s => s);
+  | Symbol.Raw s => s
+  | Symbol.Malformed s => error (Symbol.malformed_msg s));
 
 in
 
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -57,7 +57,7 @@
   let val res =
     str
     |> Source.of_string_limited 8000
-    |> Symbol.source {do_recover = false}
+    |> Symbol.source
     |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
     |> Token.source_proper
     |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
@@ -79,7 +79,7 @@
 
 fun consistent_name name name' =
   if name = name' then ()
-  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
-    " does not agree with theory name " ^ quote name');
+  else error ("Bad file name " ^ quote (Path.implode (thy_path name)) ^
+    " for theory " ^ quote name');
 
 end;
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -32,14 +32,11 @@
 
 (* parse *)
 
-fun token_source lexs pos src =
-  Symbol.source {do_recover = true} src
-  |> Token.source {do_recover = SOME false} (K lexs) pos;
+fun token_source lexs pos =
+  Symbol.source #> Token.source {do_recover = SOME false} (K lexs) pos;
 
-fun parse_tokens lexs pos str =
-  Source.of_string str
-  |> token_source lexs pos
-  |> Source.exhaust;
+fun parse_tokens lexs pos =
+  Source.of_string #> token_source lexs pos #> Source.exhaust;
 
 
 (* present *)
@@ -79,13 +76,17 @@
         else I;
     in props (token_kind_markup kind) end;
 
+fun report_symbol (sym, pos) =
+  if Symbol.is_malformed sym then Position.report pos Markup.malformed else ();
+
 in
 
 fun present_token tok =
   Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
 
 fun report_token tok =
-  Position.report (Token.position_of tok) (token_markup tok);
+ (Position.report (Token.position_of tok) (token_markup tok);
+  List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok)));
 
 end;
 
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Pure/library.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -210,12 +210,12 @@
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   val gensym: string -> string
-  type stamp
+  type stamp = unit Unsynchronized.ref
   val stamp: unit -> stamp
-  type serial
+  type serial = int
   val serial: unit -> serial
   val serial_string: unit -> string
-  structure Object: sig type T end
+  structure Object: sig type T = exn end
 end;
 
 signature LIBRARY =
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Sun Nov 14 23:55:25 2010 +0100
@@ -66,7 +66,7 @@
 
 fun end_position_of (Token (_, _, (_, epos))) = epos;
 
-val is_space = symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
+val is_space = Symbol_Pos.symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
 val scan_space =
   (Scan.many1 is_space @@@ Scan.optional ($$$ "\n") []
    ||
@@ -78,11 +78,11 @@
   ((fn x => Symbol.is_ascii x andalso
       not (Symbol.is_ascii_letter x
            orelse Symbol.is_ascii_digit x
-           orelse Symbol.is_ascii_blank x)) o symbol)
-  -- Scan.many (not o Symbol.is_ascii_blank o symbol)
+           orelse Symbol.is_ascii_blank x)) o Symbol_Pos.symbol)
+  -- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
   >> (token AsciiSymbol o op ::);
 
-fun not_contains xs c = not (member (op =) (explode xs) (symbol c));
+fun not_contains xs c = not (member (op =) (explode xs) (Symbol_Pos.symbol c));
 val scan_comment =
   $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
   >> token Comment;
@@ -90,7 +90,7 @@
 fun tokenize syms =
   let
     val scanner =
-      Scan.one (Symbol.is_symbolic o symbol) >> (token Symbol o single) ||
+      Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> (token Symbol o single) ||
       scan_comment ||
       scan_space ||
       scan_code ||
diff -r b8482ff0bc92 -r b6f1da38fa24 src/Tools/jEdit/README
--- a/src/Tools/jEdit/README	Fri Nov 12 17:28:43 2010 +0100
+++ b/src/Tools/jEdit/README	Sun Nov 14 23:55:25 2010 +0100
@@ -15,9 +15,9 @@
   http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
 
 
-Some limitations of the current implementation (as of Isabelle2009-2):
+Some limitations of the current implementation:
 
-  * No provisions for editing multiple theory files.
+  * No provisions for theory file dependencies inside the editor.
 
   * No reclaiming of old/unused document versions.  Memory will fill
     up eventually, both on the JVM and ML side.