hardwired abbreviations for standard control symbols;
authorwenzelm
Sat, 18 Jun 2011 18:17:08 +0200
changeset 43445 270bbbcda059
parent 43444 f744902b4681
child 43446 9064e1a72c5d
hardwired abbreviations for standard control symbols;
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)