src/Pure/Isar/outer_syntax.scala
changeset 58900 1435cc20b022
parent 58899 0a793c580685
child 58901 47809a811eba
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 15:32:11 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 16:57:12 2014 +0100
     1.3 @@ -74,66 +74,25 @@
     1.4  }
     1.5  
     1.6  final class Outer_Syntax private(
     1.7 -  keywords: Map[String, (String, List[String])] = Map.empty,
     1.8 -  minor: Scan.Lexicon = Scan.Lexicon.empty,
     1.9 -  major: Scan.Lexicon = Scan.Lexicon.empty,
    1.10 +  val keywords: Keyword.Keywords = Keyword.Keywords.empty,
    1.11    val completion: Completion = Completion.empty,
    1.12    val language_context: Completion.Language_Context = Completion.Language_Context.outer,
    1.13    val has_tokens: Boolean = true) extends Prover.Syntax
    1.14  {
    1.15    /** syntax content **/
    1.16  
    1.17 -  override def toString: String =
    1.18 -    (for ((name, (kind, files)) <- keywords) yield {
    1.19 -      if (kind == Keyword.MINOR) quote(name)
    1.20 -      else
    1.21 -        quote(name) + " :: " + quote(kind) +
    1.22 -        (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
    1.23 -    }).toList.sorted.mkString("keywords\n  ", " and\n  ", "")
    1.24 -
    1.25 -
    1.26 -  /* keyword kind */
    1.27 -
    1.28 -  def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
    1.29 -  def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
    1.30 -
    1.31 -  def is_command(name: String): Boolean =
    1.32 -    keyword_kind(name) match {
    1.33 -      case Some(kind) => kind != Keyword.MINOR
    1.34 -      case None => false
    1.35 -    }
    1.36 -
    1.37 -  def command_kind(token: Token, pred: String => Boolean): Boolean =
    1.38 -    token.is_command && is_command(token.source) &&
    1.39 -      pred(keyword_kind(token.source).get)
    1.40 -
    1.41 -
    1.42 -  /* load commands */
    1.43 -
    1.44 -  def load_command(name: String): Option[List[String]] =
    1.45 -    keywords.get(name) match {
    1.46 -      case Some((Keyword.THY_LOAD, exts)) => Some(exts)
    1.47 -      case _ => None
    1.48 -    }
    1.49 -
    1.50 -  val load_commands: List[(String, List[String])] =
    1.51 -    (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
    1.52 -
    1.53 -  def load_commands_in(text: String): Boolean =
    1.54 -    load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
    1.55 +  override def toString: String = keywords.toString
    1.56  
    1.57  
    1.58    /* add keywords */
    1.59  
    1.60    def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
    1.61    {
    1.62 -    val keywords1 = keywords + (name -> kind)
    1.63 -    val (minor1, major1) =
    1.64 -      if (kind._1 == Keyword.MINOR) (minor + name, major) else (minor, major + name)
    1.65 +    val keywords1 = keywords + (name, kind)
    1.66      val completion1 =
    1.67        if (replace == Some("")) completion
    1.68        else completion + (name, replace getOrElse name)
    1.69 -    new Outer_Syntax(keywords1, minor1, major1, completion1, language_context, true)
    1.70 +    new Outer_Syntax(keywords1, completion1, language_context, true)
    1.71    }
    1.72  
    1.73    def + (name: String, kind: (String, List[String])): Outer_Syntax =
    1.74 @@ -157,14 +116,20 @@
    1.75      }
    1.76  
    1.77  
    1.78 +  /* load commands */
    1.79 +
    1.80 +  def load_command(name: String): Option[List[String]] = keywords.load_command(name)
    1.81 +  def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
    1.82 +
    1.83 +
    1.84    /* language context */
    1.85  
    1.86    def set_language_context(context: Completion.Language_Context): Outer_Syntax =
    1.87 -    new Outer_Syntax(keywords, minor, major, completion, context, has_tokens)
    1.88 +    new Outer_Syntax(keywords, completion, context, has_tokens)
    1.89  
    1.90    def no_tokens: Outer_Syntax =
    1.91    {
    1.92 -    require(keywords.isEmpty && minor.isEmpty && major.isEmpty)
    1.93 +    require(keywords.is_empty)
    1.94      new Outer_Syntax(
    1.95        completion = completion,
    1.96        language_context = language_context,
    1.97 @@ -184,7 +149,7 @@
    1.98      val command1 = tokens.exists(_.is_command)
    1.99  
   1.100      val depth1 =
   1.101 -      if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
   1.102 +      if (tokens.exists(tok => keywords.command_kind(tok, Keyword.theory))) 0
   1.103        else if (command1) struct.after_span_depth
   1.104        else struct.span_depth
   1.105  
   1.106 @@ -192,11 +157,16 @@
   1.107        ((struct.span_depth, struct.after_span_depth) /: tokens) {
   1.108          case ((x, y), tok) =>
   1.109            if (tok.is_command) {
   1.110 -            if (command_kind(tok, Keyword.theory_goal)) (2, 1)
   1.111 -            else if (command_kind(tok, Keyword.theory)) (1, 0)
   1.112 -            else if (command_kind(tok, Keyword.proof_goal) || tok.is_begin_block) (y + 2, y + 1)
   1.113 -            else if (command_kind(tok, Keyword.qed) || tok.is_end_block) (y + 1, y - 1)
   1.114 -            else if (command_kind(tok, Keyword.qed_global)) (1, 0)
   1.115 +            if (keywords.command_kind(tok, Keyword.theory_goal))
   1.116 +              (2, 1)
   1.117 +            else if (keywords.command_kind(tok, Keyword.theory))
   1.118 +              (1, 0)
   1.119 +            else if (keywords.command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
   1.120 +              (y + 2, y + 1)
   1.121 +            else if (keywords.command_kind(tok, Keyword.qed) || tok.is_end_block)
   1.122 +              (y + 1, y - 1)
   1.123 +            else if (keywords.command_kind(tok, Keyword.qed_global))
   1.124 +              (1, 0)
   1.125              else (x, y)
   1.126            }
   1.127            else (x, y)
   1.128 @@ -211,7 +181,7 @@
   1.129    def scan(input: CharSequence): List[Token] =
   1.130    {
   1.131      val in: Reader[Char] = new CharSequenceReader(input)
   1.132 -    Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(minor, major)), in) match {
   1.133 +    Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(keywords)), in) match {
   1.134        case Token.Parsers.Success(tokens, _) => tokens
   1.135        case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
   1.136      }
   1.137 @@ -223,7 +193,7 @@
   1.138      val toks = new mutable.ListBuffer[Token]
   1.139      var ctxt = context
   1.140      while (!in.atEnd) {
   1.141 -      Token.Parsers.parse(Token.Parsers.token_line(minor, major, ctxt), in) match {
   1.142 +      Token.Parsers.parse(Token.Parsers.token_line(keywords, ctxt), in) match {
   1.143          case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
   1.144          case Token.Parsers.NoSuccess(_, rest) =>
   1.145            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
   1.146 @@ -284,7 +254,7 @@
   1.147        case "subsection" => Some(2)
   1.148        case "subsubsection" => Some(3)
   1.149        case _ =>
   1.150 -        keyword_kind(command.name) match {
   1.151 +        keywords.kind(command.name) match {
   1.152            case Some(kind) if Keyword.theory(kind) => Some(4)
   1.153            case _ => None
   1.154          }