--- a/Admin/PLATFORMS Sun Nov 28 08:41:16 2010 -0800
+++ b/Admin/PLATFORMS Sun Nov 28 20:12:22 2010 +0100
@@ -29,12 +29,12 @@
following reference versions (which have been selected to be neither
too old nor too new):
- x86-linux Ubuntu 8.04 LTS Server
- x86-darwin Mac OS Leopard
- x86-cygwin Cygwin 1.7
+ x86-linux SuSE 11.0 (atbroy51)
+ x86-darwin Mac OS Leopard (macbroy6)
+ x86-cygwin Cygwin 1.7 (atbroy102)
- x86_64-linux Ubuntu 8.04 LTS Server (64)
- x86_64-darwin Mac OS Leopard
+ x86_64-linux SuSE 11.0 (atbroy100)
+ x86_64-darwin Mac OS Leopard (macbroy6)
All of the above platforms are 100% supported by Isabelle -- end-users
should not have to care about the differences at all. There are also
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/java/README Sun Nov 28 20:12:22 2010 +0100
@@ -0,0 +1,2 @@
+This is JRE 1.6.0_22 for Linux and Linux x86 from
+http://www.java.com/en/download/manual.jsp
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/java/etc/settings Sun Nov 28 20:12:22 2010 +0100
@@ -0,0 +1,2 @@
+JAVA_HOME="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/jre1.6.0_22"
+ISABELLE_JAVA="$JAVA_HOME/bin/java"
--- a/src/Pure/Isar/parse.ML Sun Nov 28 08:41:16 2010 -0800
+++ b/src/Pure/Isar/parse.ML Sun Nov 28 20:12:22 2010 +0100
@@ -90,6 +90,7 @@
val prop_group: string parser
val term: string parser
val prop: string parser
+ val literal_fact: string parser
val propp: (string * string list) parser
val termp: (string * string list) parser
val target: xstring parser
@@ -315,14 +316,16 @@
(* terms *)
-val trm = short_ident || long_ident || sym_ident || term_var || number || string;
+val tm = short_ident || long_ident || sym_ident || term_var || number || string;
-val term_group = group "term" trm;
-val prop_group = group "proposition" trm;
+val term_group = group "term" tm;
+val prop_group = group "proposition" tm;
val term = inner_syntax term_group;
val prop = inner_syntax prop_group;
+val literal_fact = inner_syntax (group "literal fact" alt_string);
+
(* patterns *)
--- a/src/Pure/Isar/parse_spec.ML Sun Nov 28 08:41:16 2010 -0800
+++ b/src/Pure/Isar/parse_spec.ML Sun Nov 28 20:12:22 2010 +0100
@@ -61,7 +61,7 @@
val xthm =
Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
- (Parse.alt_string >> Facts.Fact ||
+ (Parse.literal_fact >> Facts.Fact ||
Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
val xthms1 = Scan.repeat1 xthm;
--- a/src/Pure/Thy/thy_syntax.scala Sun Nov 28 08:41:16 2010 -0800
+++ b/src/Pure/Thy/thy_syntax.scala Sun Nov 28 20:12:22 2010 +0100
@@ -27,7 +27,7 @@
def length: Int = command.length
}
- def parse_sections(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
+ def parse(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
{
/* stack operations */
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Sun Nov 28 08:41:16 2010 -0800
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Sun Nov 28 20:12:22 2010 +0100
@@ -5,7 +5,7 @@
buffer.lineSeparator=\n
buffer.maxLineLen=100
buffer.noTabs=true
-buffer.sidekick.keystroke-parse=true
+buffer.sidekick.keystroke-parse=false
buffer.tabSize=2
console.encoding=UTF-8
console.font=IsabelleText
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Nov 28 08:41:16 2010 -0800
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Nov 28 20:12:22 2010 +0100
@@ -138,7 +138,7 @@
}
val text = Isabelle.buffer_text(model.buffer)
- val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text)
+ val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
make_tree(0, structure) foreach (node => data.root.add(node))
}