diff -r fdd6e68e29d9 -r 28083e9f8d1d src/Pure/General/symbol.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/symbol.scala	Fri Aug 15 21:53:40 2008 +0200
@@ -0,0 +1,30 @@
+/*  Title:      Pure/General/symbol.scala
+    ID:         $Id$
+    Author:     Makarius
+
+Basic support for Isabelle symbols.
+*/
+
+package isabelle
+
+import java.util.regex.Pattern
+
+
+object Symbol {
+
+  /* Regular expressions */
+
+  private def compile(s: String) =
+    Pattern.compile(s, Pattern.COMMENTS | Pattern.DOTALL)
+
+  private val symbol_src = """ \\ \\? < (?:
+      \^? [A-Za-z][A-Za-z0-9_']* |
+      \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >"""
+
+  private val bad_symbol_src = "(?!" + symbol_src + ")" +
+    """ \\ \\? < (?: (?! \p{Space} | ["`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
+
+  val symbol_pattern = compile(symbol_src)
+  val bad_symbol_pattern = compile(bad_symbol_src)
+  val pattern = compile(symbol_src + "|" + bad_symbol_src + "| .")
+}