src/Pure/Thy/thy_header.scala
author wenzelm
Fri, 07 Nov 2014 16:36:55 +0100
changeset 58928 23d0ffd48006
parent 58908 58bedbc18915
child 58999 ed09ae4ea2d8
permissions -rw-r--r--
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
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"
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    27
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    28
  val THEORY = "theory"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    29
  val IMPORTS = "imports"
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    30
  val KEYWORDS = "keywords"
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    31
  val AND = "and"
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    32
  val BEGIN = "begin"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    33
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    34
  private val bootstrap_header: Keywords =
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    35
    List(
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    36
      ("%", None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    37
      ("(", None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    38
      (")", None, None),
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
      (AND, None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    43
      (BEGIN, None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    44
      (IMPORTS, None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    45
      (KEYWORDS, None, None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    46
      (HEADER, Some(((Keyword.HEADING, Nil), Nil)), None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    47
      (CHAPTER, Some(((Keyword.HEADING, Nil), Nil)), None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    48
      (SECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    49
      (SUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    50
      (SUBSUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    51
      (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
    52
      ("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
    53
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    54
  private val bootstrap_keywords =
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    55
    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
    56
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    57
  def bootstrap_syntax(): Outer_Syntax =
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    58
    Outer_Syntax.init().add_keywords(bootstrap_header)
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
    59
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 36956
diff changeset
    60
44160
8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents: 44159
diff changeset
    61
  /* 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
    62
44225
a8f921e6484f more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents: 44222
diff changeset
    63
  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
    64
  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
    65
44225
a8f921e6484f more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents: 44222
diff changeset
    66
  def base_name(s: String): String =
a8f921e6484f more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents: 44222
diff changeset
    67
    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
    68
44222
9d5ef6cd4ee1 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents: 44185
diff changeset
    69
  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
    70
    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
    71
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    72
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    73
  /* header */
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    74
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
    75
  val header: Parser[Thy_Header] =
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    76
  {
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
    77
    val file_name = atom("file name", _.is_name)
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    78
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    79
    val opt_files =
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    80
      $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    81
      success(Nil)
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    82
    val keyword_spec =
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    83
      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
    84
      { case x ~ y ~ z => ((x, y), z) }
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48706
diff changeset
    85
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    86
    val keyword_decl =
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48882
diff changeset
    87
      rep1(string) ~
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    88
      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    89
      opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48882
diff changeset
    90
      { case xs ~ y ~ z => xs.map((_, y, z)) }
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
    91
    val keyword_decls =
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    92
      keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
    93
      { case xs ~ yss => (xs :: yss).flatten }
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    94
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    95
    val file =
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
    96
      $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44163
diff changeset
    97
      file_name ^^ (x => (x, true))
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    98
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    99
    val args =
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
   100
      theory_name ~
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   101
      (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   102
        { case None => Nil case Some(_ ~ xs) => xs }) ~
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   103
      (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
   104
        { case None => Nil case Some(_ ~ xs) => xs }) ~
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   105
      $$$(BEGIN) ^^
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
   106
      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   107
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
   108
    val heading =
58907
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   109
      (command(HEADER) |
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   110
        command(CHAPTER) |
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   111
        command(SECTION) |
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   112
        command(SUBSECTION) |
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   113
        command(SUBSUBSECTION)) ~
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
   114
      tags ~! document_source
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
   115
58907
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58903
diff changeset
   116
    (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   117
  }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   118
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   119
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   120
  /* read -- lazy scanning */
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   121
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   122
  def read(reader: Reader[Char]): Thy_Header =
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   123
  {
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
   124
    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
   125
    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
   126
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
   127
    @tailrec def scan_to_begin(in: Reader[Char])
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   128
    {
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   129
      token(in) match {
55494
009b71c1ed23 tuned signature (in accordance to ML version);
wenzelm
parents: 55492
diff changeset
   130
        case Token.Parsers.Success(tok, rest) =>
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   131
          toks += tok
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
   132
          if (!tok.is_begin) scan_to_begin(rest)
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   133
        case _ =>
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   134
      }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   135
    }
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
   136
    scan_to_begin(reader)
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   137
36956
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36948
diff changeset
   138
    parse(commit(header), Token.reader(toks.toList)) match {
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   139
      case Success(result, _) => result
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   140
      case bad => error(bad.toString)
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   141
    }
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   142
  }
43611
21a57a0c5f25 more general theory header parsing;
wenzelm
parents: 41535
diff changeset
   143
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   144
  def read(source: CharSequence): Thy_Header =
43646
598b2c6ce13f Thy_Header.read convenience;
wenzelm
parents: 43611
diff changeset
   145
    read(new CharSequenceReader(source))
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   146
}
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   147
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   148
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44163
diff changeset
   149
sealed case class Thy_Header(
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48882
diff changeset
   150
  name: String,
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48882
diff changeset
   151
  imports: List[String],
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
   152
  keywords: Thy_Header.Keywords)
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   153
{
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   154
  def map(f: String => String): Thy_Header =
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
   155
    Thy_Header(f(name), imports.map(f), keywords)
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   156
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   157
  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
   158
  {
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   159
    val f = Symbol.decode _
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   160
    Thy_Header(f(name), imports.map(f),
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56801
diff changeset
   161
      keywords.map({ case (a, b, c) =>
58899
0a793c580685 clarified minor/major lexicon (like ML version);
wenzelm
parents: 58868
diff changeset
   162
        (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
   163
  }
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   164
}
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   165