somewhat adhoc replacement for 'thus' and 'hence';
authorwenzelm
Sat Nov 13 22:33:07 2010 +0100 (2010-11-13)
changeset 40533e38e80686ce5
parent 40532 f51c478ef85a
child 40534 9e196062bf88
somewhat adhoc replacement for 'thus' and 'hence';
complete words as short as 2 characters, e.g. "Un";
src/Pure/Isar/outer_syntax.scala
src/Pure/System/session.scala
src/Pure/Thy/completion.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Nov 13 21:46:24 2010 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Nov 13 22:33:07 2010 +0100
     1.3 @@ -18,11 +18,11 @@
     1.4  
     1.5    def keyword_kind(name: String): Option[String] = keywords.get(name)
     1.6  
     1.7 -  def + (name: String, kind: String): Outer_Syntax =
     1.8 +  def + (name: String, kind: String, replace: String): Outer_Syntax =
     1.9    {
    1.10      val new_keywords = keywords + (name -> kind)
    1.11      val new_lexicon = lexicon + name
    1.12 -    val new_completion = completion + name
    1.13 +    val new_completion = completion + (name, replace)
    1.14      new Outer_Syntax(symbols) {
    1.15        override val lexicon = new_lexicon
    1.16        override val keywords = new_keywords
    1.17 @@ -30,6 +30,8 @@
    1.18      }
    1.19    }
    1.20  
    1.21 +  def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
    1.22 +
    1.23    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    1.24  
    1.25    def is_command(name: String): Boolean =
     2.1 --- a/src/Pure/System/session.scala	Sat Nov 13 21:46:24 2010 +0100
     2.2 +++ b/src/Pure/System/session.scala	Sat Nov 13 22:33:07 2010 +0100
     2.3 @@ -208,7 +208,12 @@
     2.4          case _ =>
     2.5            if (result.is_syslog) {
     2.6              reverse_syslog ::= result.message
     2.7 -            if (result.is_ready) phase = Session.Ready
     2.8 +            if (result.is_ready) {
     2.9 +              // FIXME move to ML side
    2.10 +              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
    2.11 +              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
    2.12 +              phase = Session.Ready
    2.13 +            }
    2.14              else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
    2.15              else if (result.is_exit) phase = Session.Inactive
    2.16            }
     3.1 --- a/src/Pure/Thy/completion.scala	Sat Nov 13 21:46:24 2010 +0100
     3.2 +++ b/src/Pure/Thy/completion.scala	Sat Nov 13 22:33:07 2010 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4  
     3.5      def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
     3.6      def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
     3.7 -    def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
     3.8 +    def word: Parser[String] = "[a-zA-Z0-9_']{2,}".r
     3.9  
    3.10      def read(in: CharSequence): Option[String] =
    3.11      {
    3.12 @@ -49,17 +49,19 @@
    3.13  
    3.14    /* adding stuff */
    3.15  
    3.16 -  def + (keyword: String): Completion =
    3.17 +  def + (keyword: String, replace: String): Completion =
    3.18    {
    3.19      val old = this
    3.20      new Completion {
    3.21        override val words_lex = old.words_lex + keyword
    3.22 -      override val words_map = old.words_map + (keyword -> keyword)
    3.23 +      override val words_map = old.words_map + (keyword -> replace)
    3.24        override val abbrevs_lex = old.abbrevs_lex
    3.25        override val abbrevs_map = old.abbrevs_map
    3.26      }
    3.27    }
    3.28  
    3.29 +  def + (keyword: String): Completion = this + (keyword, keyword)
    3.30 +
    3.31    def + (symbols: Symbol.Interpretation): Completion =
    3.32    {
    3.33      val words =