# HG changeset patch
# User wenzelm
# Date 1290971542 -3600
# Node ID 0562a0a5bb9339138375b05040d1b4d07f53bcc0
# Parent  1b15d1805b7288be80a2886ccc3ac6c5f4145907# Parent  d21aedaa91e7470a139d0aba868d7cc190c46728
merged

diff -r 1b15d1805b72 -r 0562a0a5bb93 Admin/PLATFORMS
--- 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
diff -r 1b15d1805b72 -r 0562a0a5bb93 Admin/java/README
--- /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
diff -r 1b15d1805b72 -r 0562a0a5bb93 Admin/java/etc/settings
--- /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"
diff -r 1b15d1805b72 -r 0562a0a5bb93 src/Pure/Isar/parse.ML
--- 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 *)
 
diff -r 1b15d1805b72 -r 0562a0a5bb93 src/Pure/Isar/parse_spec.ML
--- 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;
diff -r 1b15d1805b72 -r 0562a0a5bb93 src/Pure/Thy/thy_syntax.scala
--- 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 */
 
diff -r 1b15d1805b72 -r 0562a0a5bb93 src/Tools/jEdit/dist-template/properties/jedit.props
--- 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
diff -r 1b15d1805b72 -r 0562a0a5bb93 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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))
   }