src/Pure/Thy/thy_header.scala
author wenzelm
Thu Nov 13 23:45:15 2014 +0100 (2014-11-13)
changeset 58999 ed09ae4ea2d8
parent 58928 23d0ffd48006
child 59694 d2bb4b5ed862
permissions -rw-r--r--
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
discontinued obsolete 'txt_raw' (superseded by 'text_raw');
eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds);
'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind;
changed tagging of diagnostic commands within proof;
     1 /*  Title:      Pure/Thy/thy_header.scala
     2     Author:     Makarius
     3 
     4 Static theory header information.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.annotation.tailrec
    11 import scala.collection.mutable
    12 import scala.util.parsing.input.{Reader, CharSequenceReader}
    13 import scala.util.matching.Regex
    14 
    15 
    16 object Thy_Header extends Parse.Parser
    17 {
    18   /* bootstrap keywords */
    19 
    20   type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
    21 
    22   val HEADER = "header"
    23   val CHAPTER = "chapter"
    24   val SECTION = "section"
    25   val SUBSECTION = "subsection"
    26   val SUBSUBSECTION = "subsubsection"
    27   val TEXT = "text"
    28   val TXT = "txt"
    29   val TEXT_RAW = "text_raw"
    30 
    31   val THEORY = "theory"
    32   val IMPORTS = "imports"
    33   val KEYWORDS = "keywords"
    34   val AND = "and"
    35   val BEGIN = "begin"
    36 
    37   private val bootstrap_header: Keywords =
    38     List(
    39       ("%", None, None),
    40       ("(", None, None),
    41       (")", None, None),
    42       (",", None, None),
    43       ("::", None, None),
    44       ("==", None, None),
    45       (AND, None, None),
    46       (BEGIN, None, None),
    47       (IMPORTS, None, None),
    48       (KEYWORDS, None, None),
    49       (HEADER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    50       (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    51       (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    52       (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    53       (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    54       (TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    55       (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    56       (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
    57       (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
    58       ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
    59 
    60   private val bootstrap_keywords =
    61     Keyword.Keywords.empty.add_keywords(bootstrap_header)
    62 
    63   def bootstrap_syntax(): Outer_Syntax =
    64     Outer_Syntax.init().add_keywords(bootstrap_header)
    65 
    66 
    67   /* theory file name */
    68 
    69   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
    70   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    71 
    72   def base_name(s: String): String =
    73     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    74 
    75   def thy_name(s: String): Option[String] =
    76     s match { case Thy_Name(name) => Some(name) case _ => None }
    77 
    78 
    79   /* header */
    80 
    81   val header: Parser[Thy_Header] =
    82   {
    83     val file_name = atom("file name", _.is_name)
    84 
    85     val opt_files =
    86       $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
    87       success(Nil)
    88     val keyword_spec =
    89       atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    90       { case x ~ y ~ z => ((x, y), z) }
    91 
    92     val keyword_decl =
    93       rep1(string) ~
    94       opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    95       opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
    96       { case xs ~ y ~ z => xs.map((_, y, z)) }
    97     val keyword_decls =
    98       keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    99       { case xs ~ yss => (xs :: yss).flatten }
   100 
   101     val file =
   102       $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
   103       file_name ^^ (x => (x, true))
   104 
   105     val args =
   106       theory_name ~
   107       (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
   108         { case None => Nil case Some(_ ~ xs) => xs }) ~
   109       (opt($$$(KEYWORDS) ~! keyword_decls) ^^
   110         { case None => Nil case Some(_ ~ xs) => xs }) ~
   111       $$$(BEGIN) ^^
   112       { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
   113 
   114     val heading =
   115       (command(HEADER) |
   116         command(CHAPTER) |
   117         command(SECTION) |
   118         command(SUBSECTION) |
   119         command(SUBSUBSECTION) |
   120         command(TEXT) |
   121         command(TXT) |
   122         command(TEXT_RAW)) ~
   123       tags ~! document_source
   124 
   125     (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   126   }
   127 
   128 
   129   /* read -- lazy scanning */
   130 
   131   def read(reader: Reader[Char]): Thy_Header =
   132   {
   133     val token = Token.Parsers.token(bootstrap_keywords)
   134     val toks = new mutable.ListBuffer[Token]
   135 
   136     @tailrec def scan_to_begin(in: Reader[Char])
   137     {
   138       token(in) match {
   139         case Token.Parsers.Success(tok, rest) =>
   140           toks += tok
   141           if (!tok.is_begin) scan_to_begin(rest)
   142         case _ =>
   143       }
   144     }
   145     scan_to_begin(reader)
   146 
   147     parse(commit(header), Token.reader(toks.toList)) match {
   148       case Success(result, _) => result
   149       case bad => error(bad.toString)
   150     }
   151   }
   152 
   153   def read(source: CharSequence): Thy_Header =
   154     read(new CharSequenceReader(source))
   155 }
   156 
   157 
   158 sealed case class Thy_Header(
   159   name: String,
   160   imports: List[String],
   161   keywords: Thy_Header.Keywords)
   162 {
   163   def map(f: String => String): Thy_Header =
   164     Thy_Header(f(name), imports.map(f), keywords)
   165 
   166   def decode_symbols: Thy_Header =
   167   {
   168     val f = Symbol.decode _
   169     Thy_Header(f(name), imports.map(f),
   170       keywords.map({ case (a, b, c) =>
   171         (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
   172   }
   173 }
   174