# HG changeset patch
# User wenzelm
# Date 1308413828 -7200
# Node ID 270bbbcda0598dbbbe149455a480ca69dfc3579e
# Parent  f744902b46812bed66e097e1274ad56724f0fc6b
hardwired abbreviations for standard control symbols;

diff -r f744902b4681 -r 270bbbcda059 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Sat Jun 18 17:42:28 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Jun 18 18:17:08 2011 +0200
@@ -15,7 +15,14 @@
 {
   protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
   protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
-  lazy val completion: Completion = new Completion + symbols  // FIXME !?
+  lazy val completion: Completion = // FIXME odd initialization
+    new Completion + symbols +
+      ("sub", "\\<^sub>") +
+      ("sup", "\\<^sup>") +
+      ("isub", "\\<^isub>") +
+      ("isup", "\\<^isup>") +
+      ("bold", "\\<^bold>") +
+      ("loc", "\\<^loc>")
 
   def keyword_kind(name: String): Option[String] = keywords.get(name)