src/Pure/Thy/thy_header.scala
author wenzelm
Thu, 16 Apr 2015 15:00:03 +0200
changeset 60095 35f626b11422
parent 59736 5c1a0069b9d3
child 60215 5fb4990dfc73
permissions -rw-r--r--
more explicit bootstrap_thy; clarified error;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/thy_header.scala
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     3
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
     4
Static theory header information.
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     5
*/
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     6
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     7
package isabelle
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     8
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
     9
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
    10
import scala.annotation.tailrec
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    11
import scala.collection.mutable
43646
598b2c6ce13f Thy_Header.read convenience;
wenzelm
parents: 43611
diff changeset
    12
import scala.util.parsing.input.{Reader, CharSequenceReader}
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 36956
diff changeset
    13
import scala.util.matching.Regex
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    14
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    15
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43652
diff changeset
    16
object Thy_Header extends Parse.Parser
32450
375db037f4d2 misc tuning;
wenzelm
parents: 29140
diff changeset
    17
{
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    18
  /* bootstrap keywords */
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    19
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    20
  type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    21
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    22
  val HEADER = "header"
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    23
  val CHAPTER = "chapter"
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    24
  val SECTION = "section"
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    25
  val SUBSECTION = "subsection"
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    26
  val SUBSUBSECTION = "subsubsection"
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    27
  val TEXT = "text"
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    28
  val TXT = "txt"
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    29
  val TEXT_RAW = "text_raw"
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    30
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    31
  val THEORY = "theory"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    32
  val IMPORTS = "imports"
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    33
  val KEYWORDS = "keywords"
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    34
  val AND = "and"
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    35
  val BEGIN = "begin"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    36
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    37
  private val bootstrap_header: Keywords =
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    38
    List(
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    39
      ("%", None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    40
      ("(", None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    41
      (")", None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    42
      (",", None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    43
      ("::", None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    44
      ("==", None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    45
      (AND, None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    46
      (BEGIN, None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    47
      (IMPORTS, None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    48
      (KEYWORDS, None, None),
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    49
      (HEADER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    50
      (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    51
      (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    52
      (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    53
      (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    54
      (TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    55
      (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
    56
      (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    57
      (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    58
      ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    59
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    60
  private val bootstrap_keywords =
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    61
    Keyword.Keywords.empty.add_keywords(bootstrap_header)
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    62
59736
5c1a0069b9d3 tight span for theory header, which is relevant for error positions (including semantic completion);
wenzelm
parents: 59705
diff changeset
    63
  lazy val bootstrap_syntax: Outer_Syntax =
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    64
    Outer_Syntax.init().add_keywords(bootstrap_header)
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
    65
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 36956
diff changeset
    66
44160
8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents: 44159
diff changeset
    67
  /* theory file name */
8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents: 44159
diff changeset
    68
44225
a8f921e6484f more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents: 44222
diff changeset
    69
  private val Base_Name = new Regex(""".*?([^/\\:]+)""")
44222
9d5ef6cd4ee1 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents: 44185
diff changeset
    70
  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
44160
8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents: 44159
diff changeset
    71
44225
a8f921e6484f more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents: 44222
diff changeset
    72
  def base_name(s: String): String =
a8f921e6484f more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents: 44222
diff changeset
    73
    s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
a8f921e6484f more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents: 44222
diff changeset
    74
44222
9d5ef6cd4ee1 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents: 44185
diff changeset
    75
  def thy_name(s: String): Option[String] =
9d5ef6cd4ee1 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents: 44185
diff changeset
    76
    s match { case Thy_Name(name) => Some(name) case _ => None }
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 36956
diff changeset
    77
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    78
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    79
  /* header */
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    80
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
    81
  val header: Parser[Thy_Header] =
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    82
  {
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    83
    val opt_files =
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    84
      $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    85
      success(Nil)
59694
d2bb4b5ed862 misc tuning -- more uniform ML vs. Scala;
wenzelm
parents: 58999
diff changeset
    86
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    87
    val keyword_spec =
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    88
      atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    89
      { case x ~ y ~ z => ((x, y), z) }
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    90
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    91
    val keyword_decl =
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48882
diff changeset
    92
      rep1(string) ~
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    93
      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    94
      opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48882
diff changeset
    95
      { case xs ~ y ~ z => xs.map((_, y, z)) }
59694
d2bb4b5ed862 misc tuning -- more uniform ML vs. Scala;
wenzelm
parents: 58999
diff changeset
    96
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
    97
    val keyword_decls =
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    98
      keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
    99
      { case xs ~ yss => (xs :: yss).flatten }
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
   100
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   101
    val args =
59694
d2bb4b5ed862 misc tuning -- more uniform ML vs. Scala;
wenzelm
parents: 58999
diff changeset
   102
      position(theory_name) ~
d2bb4b5ed862 misc tuning -- more uniform ML vs. Scala;
wenzelm
parents: 58999
diff changeset
   103
      (opt($$$(IMPORTS) ~! (rep1(position(theory_xname)))) ^^
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   104
        { case None => Nil case Some(_ ~ xs) => xs }) ~
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   105
      (opt($$$(KEYWORDS) ~! keyword_decls) ^^
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   106
        { case None => Nil case Some(_ ~ xs) => xs }) ~
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   107
      $$$(BEGIN) ^^
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
   108
      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   109
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
   110
    val heading =
58907
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   111
      (command(HEADER) |
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   112
        command(CHAPTER) |
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   113
        command(SECTION) |
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   114
        command(SUBSECTION) |
58999
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
   115
        command(SUBSUBSECTION) |
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
   116
        command(TEXT) |
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
   117
        command(TXT) |
ed09ae4ea2d8 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents: 58928
diff changeset
   118
        command(TEXT_RAW)) ~
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
   119
      tags ~! document_source
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
   120
58907
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   121
    (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   122
  }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   123
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   124
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   125
  /* read -- lazy scanning */
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   126
59705
740a0ca7e09b clarified span position;
wenzelm
parents: 59695
diff changeset
   127
  def read(reader: Reader[Char], start: Token.Pos): Thy_Header =
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   128
  {
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
   129
    val token = Token.Parsers.token(bootstrap_keywords)
36956
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36948
diff changeset
   130
    val toks = new mutable.ListBuffer[Token]
34188
fbfc18be1f8c scan: operate on file (via Scan.byte_reader), more robust exception handling;
wenzelm
parents: 34169
diff changeset
   131
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
   132
    @tailrec def scan_to_begin(in: Reader[Char])
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   133
    {
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   134
      token(in) match {
55494
009b71c1ed23 tuned signature (in accordance to ML version);
wenzelm
parents: 55492
diff changeset
   135
        case Token.Parsers.Success(tok, rest) =>
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   136
          toks += tok
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
   137
          if (!tok.is_begin) scan_to_begin(rest)
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   138
        case _ =>
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   139
      }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   140
    }
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
   141
    scan_to_begin(reader)
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   142
59705
740a0ca7e09b clarified span position;
wenzelm
parents: 59695
diff changeset
   143
    parse(commit(header), Token.reader(toks.toList, start)) match {
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   144
      case Success(result, _) => result
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   145
      case bad => error(bad.toString)
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   146
    }
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   147
  }
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
   148
59705
740a0ca7e09b clarified span position;
wenzelm
parents: 59695
diff changeset
   149
  def read(source: CharSequence, start: Token.Pos): Thy_Header =
740a0ca7e09b clarified span position;
wenzelm
parents: 59695
diff changeset
   150
    read(new CharSequenceReader(source), start)
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   151
}
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   152
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   153
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44163
diff changeset
   154
sealed case class Thy_Header(
59694
d2bb4b5ed862 misc tuning -- more uniform ML vs. Scala;
wenzelm
parents: 58999
diff changeset
   155
  name: (String, Position.T),
d2bb4b5ed862 misc tuning -- more uniform ML vs. Scala;
wenzelm
parents: 58999
diff changeset
   156
  imports: List[(String, Position.T)],
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
   157
  keywords: Thy_Header.Keywords)
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   158
{
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   159
  def decode_symbols: Thy_Header =
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   160
  {
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   161
    val f = Symbol.decode _
59694
d2bb4b5ed862 misc tuning -- more uniform ML vs. Scala;
wenzelm
parents: 58999
diff changeset
   162
    Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   163
      keywords.map({ case (a, b, c) =>
58899
0a793c580685 clarified minor/major lexicon (like ML version);
wenzelm
parents: 58868
diff changeset
   164
        (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   165
  }
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   166
}