--- 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} *}
--- 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%
%
--- 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"]),
--- 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
--- 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))
--- 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;
--- 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("\\<^")
}
}
--- 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;
--- 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;
--- 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 =
--- 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
--- 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
--- 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;
--- 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
--- 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]);
--- 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
}
--- 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 =
--- 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
--- 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;
--- 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;
--- 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 =
--- 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 ||
--- 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.