src/Pure/Thy/thy_header.scala
author wenzelm
Sun, 29 Nov 2020 17:57:20 +0100
changeset 72782 98ecb951d911
parent 72779 1cc74982d038
child 72853 d0038b553e0e
permissions -rw-r--r--
more completion;
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
64824
330ec9bc4b75 tuned signature;
wenzelm
parents: 64777
diff changeset
    10
import scala.util.parsing.input.Reader
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 36956
diff changeset
    11
import scala.util.matching.Regex
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    12
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
    13
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
    14
object Thy_Header
32450
375db037f4d2 misc tuning;
wenzelm
parents: 29140
diff changeset
    15
{
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    16
  /* bootstrap keywords */
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    17
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63449
diff changeset
    18
  type Keywords = List[(String, Keyword.Spec)]
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63449
diff changeset
    19
  type Abbrevs = List[(String, String)]
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    20
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    21
  val CHAPTER = "chapter"
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    22
  val SECTION = "section"
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    23
  val SUBSECTION = "subsection"
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
    24
  val SUBSUBSECTION = "subsubsection"
61463
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 60957
diff changeset
    25
  val PARAGRAPH = "paragraph"
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 60957
diff changeset
    26
  val SUBPARAGRAPH = "subparagraph"
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"
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63449
diff changeset
    34
  val ABBREVS = "abbrevs"
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    35
  val AND = "and"
28495
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    36
  val BEGIN = "begin"
c5f86d04743b Theory header keywords.
wenzelm
parents:
diff changeset
    37
64854
f5aa712e6250 tuned signature;
wenzelm
parents: 64825
diff changeset
    38
  val bootstrap_header: Keywords =
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    39
    List(
72764
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    40
      ("%", Keyword.Spec()),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    41
      ("(", Keyword.Spec()),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    42
      (")", Keyword.Spec()),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    43
      (",", Keyword.Spec()),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    44
      ("::", Keyword.Spec()),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    45
      ("=", Keyword.Spec()),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    46
      (AND, Keyword.Spec()),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    47
      (BEGIN, Keyword.Spec(kind = Keyword.QUASI_COMMAND)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    48
      (IMPORTS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    49
      (KEYWORDS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    50
      (ABBREVS, Keyword.Spec(kind = Keyword.QUASI_COMMAND)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    51
      (CHAPTER, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    52
      (SECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    53
      (SUBSECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    54
      (SUBSUBSECTION, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    55
      (PARAGRAPH, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    56
      (SUBPARAGRAPH, Keyword.Spec(kind = Keyword.DOCUMENT_HEADING)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    57
      (TEXT, Keyword.Spec(kind = Keyword.DOCUMENT_BODY)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    58
      (TXT, Keyword.Spec(kind = Keyword.DOCUMENT_BODY)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    59
      (TEXT_RAW, Keyword.Spec(kind = Keyword.DOCUMENT_RAW)),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    60
      (THEORY, Keyword.Spec(kind = Keyword.THY_BEGIN, tags = List("theory"))),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
    61
      ("ML", Keyword.Spec(kind = Keyword.THY_DECL, tags = List("ML"))))
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    62
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    63
  private val bootstrap_keywords =
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
    64
    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
    65
67004
af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents: 66984
diff changeset
    66
  val bootstrap_syntax: Outer_Syntax =
af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents: 66984
diff changeset
    67
    Outer_Syntax.empty.add_keywords(bootstrap_header)
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
    68
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 36956
diff changeset
    69
64673
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64671
diff changeset
    70
  /* file name vs. theory name */
62895
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62849
diff changeset
    71
63022
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62969
diff changeset
    72
  val PURE = "Pure"
62895
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62849
diff changeset
    73
  val ML_BOOTSTRAP = "ML_Bootstrap"
65490
571a3ce3cc17 special theories are always global;
wenzelm
parents: 65452
diff changeset
    74
  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
63022
785a59235a15 more IDE support for Isabelle/Pure bootstrap;
wenzelm
parents: 62969
diff changeset
    75
  val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
44160
8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents: 44159
diff changeset
    76
67215
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents: 67212
diff changeset
    77
  val bootstrap_global_theories =
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents: 67212
diff changeset
    78
    (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE)
65490
571a3ce3cc17 special theories are always global;
wenzelm
parents: 65452
diff changeset
    79
65452
9e9750a7932c clarified signature;
wenzelm
parents: 65392
diff changeset
    80
  private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68841
diff changeset
    81
  private val Split_File_Name = new Regex("""(.*?)[/\\]*([^/\\:]+)""")
67212
wenzelm
parents: 67164
diff changeset
    82
  private val File_Name = new Regex(""".*?([^/\\:]+)""")
44160
8848867501fb clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents: 44159
diff changeset
    83
65526
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65490
diff changeset
    84
  def is_base_name(s: String): Boolean =
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65490
diff changeset
    85
    s != "" && !s.exists("/\\:".contains(_))
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65490
diff changeset
    86
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68841
diff changeset
    87
  def split_file_name(s: String): Option[(String, String)] =
67290
98b6cd12f963 implicit thy_load context for bibtex files;
wenzelm
parents: 67215
diff changeset
    88
    s match {
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68841
diff changeset
    89
      case Split_File_Name(s1, s2) => Some((s1, s2))
67290
98b6cd12f963 implicit thy_load context for bibtex files;
wenzelm
parents: 67215
diff changeset
    90
      case _ => None
98b6cd12f963 implicit thy_load context for bibtex files;
wenzelm
parents: 67215
diff changeset
    91
    }
98b6cd12f963 implicit thy_load context for bibtex files;
wenzelm
parents: 67215
diff changeset
    92
65452
9e9750a7932c clarified signature;
wenzelm
parents: 65392
diff changeset
    93
  def import_name(s: String): String =
67164
39f57f0757f1 clarified error;
wenzelm
parents: 67013
diff changeset
    94
    s match {
67212
wenzelm
parents: 67164
diff changeset
    95
      case File_Name(name) if !name.endsWith(".thy") => name
67164
39f57f0757f1 clarified error;
wenzelm
parents: 67013
diff changeset
    96
      case _ => error("Malformed theory import: " + quote(s))
39f57f0757f1 clarified error;
wenzelm
parents: 67013
diff changeset
    97
    }
44225
a8f921e6484f more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents: 44222
diff changeset
    98
65452
9e9750a7932c clarified signature;
wenzelm
parents: 65392
diff changeset
    99
  def theory_name(s: String): String =
62895
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62849
diff changeset
   100
    s match {
66195
bb886f13623a proper bootstrap_name (amending b42743f5b595);
wenzelm
parents: 65539
diff changeset
   101
      case Thy_File_Name(name) => bootstrap_name(name)
67212
wenzelm
parents: 67164
diff changeset
   102
      case File_Name(name) =>
67215
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents: 67212
diff changeset
   103
        if (name == Sessions.root_name) name
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents: 67212
diff changeset
   104
        else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
65452
9e9750a7932c clarified signature;
wenzelm
parents: 65392
diff changeset
   105
      case _ => ""
62895
54c2abe7e9a4 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents: 62849
diff changeset
   106
    }
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 36956
diff changeset
   107
64673
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64671
diff changeset
   108
  def is_ml_root(theory: String): Boolean =
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64671
diff changeset
   109
    ml_roots.exists({ case (_, b) => b == theory })
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64671
diff changeset
   110
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64671
diff changeset
   111
  def is_bootstrap(theory: String): Boolean =
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64671
diff changeset
   112
    bootstrap_thys.exists({ case (_, b) => b == theory })
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64671
diff changeset
   113
66195
bb886f13623a proper bootstrap_name (amending b42743f5b595);
wenzelm
parents: 65539
diff changeset
   114
  def bootstrap_name(theory: String): String =
bb886f13623a proper bootstrap_name (amending b42743f5b595);
wenzelm
parents: 65539
diff changeset
   115
    bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
bb886f13623a proper bootstrap_name (amending b42743f5b595);
wenzelm
parents: 65539
diff changeset
   116
70713
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   117
  def try_read_dir(dir: Path): List[String] =
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   118
  {
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   119
    val files =
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   120
      try { File.read_dir(dir) }
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   121
      catch { case ERROR(_) => Nil }
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   122
    for { Thy_File_Name(name) <- files } yield name
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   123
  }
fd188463066e clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents: 70638
diff changeset
   124
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   125
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   126
  /* parser */
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   127
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   128
  trait Parser extends Parse.Parser
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   129
  {
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   130
    val header: Parser[Thy_Header] =
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   131
    {
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   132
      val load_command =
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   133
        ($$$("(") ~! (position(name) <~ $$$(")")) ^^ { case _ ~ x => x }) |
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   134
          success(("", Position.none))
72748
04d5f6d769a7 more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents: 72747
diff changeset
   135
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   136
      val keyword_kind = atom("outer syntax keyword specification", _.is_name)
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   137
      val keyword_spec =
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   138
        position(keyword_kind) ~ load_command ~ tags ^^
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   139
          { case (a, b) ~ c ~ d =>
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   140
              Keyword.Spec(kind = a, kind_pos = b,
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   141
                load_command = c._1, load_command_pos = c._2, tags = d)
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   142
          }
59694
d2bb4b5ed862 misc tuning -- more uniform ML vs. Scala;
wenzelm
parents: 58999
diff changeset
   143
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   144
      val keyword_decl =
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   145
        rep1(string) ~
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   146
        opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
72764
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
   147
        { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec()))) }
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
   148
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   149
      val keyword_decls =
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   150
        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   151
        { case xs ~ yss => (xs :: yss).flatten }
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   152
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   153
      val abbrevs =
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   154
        rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   155
          { case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) }
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63449
diff changeset
   156
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   157
      val args =
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   158
        position(theory_name) ~
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   159
        (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   160
          { case None => Nil case Some(_ ~ xs) => xs }) ~
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   161
        (opt($$$(KEYWORDS) ~! keyword_decls) ^^
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   162
          { case None => Nil case Some(_ ~ xs) => xs }) ~
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   163
        (opt($$$(ABBREVS) ~! abbrevs) ^^
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   164
          { case None => Nil case Some(_ ~ xs) => xs }) ~
72779
1cc74982d038 clarified parser;
wenzelm
parents: 72778
diff changeset
   165
        $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a._1, a._2, b, c, d) }
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   166
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   167
      val heading =
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   168
        (command(CHAPTER) |
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   169
          command(SECTION) |
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   170
          command(SUBSECTION) |
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   171
          command(SUBSUBSECTION) |
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   172
          command(PARAGRAPH) |
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   173
          command(SUBPARAGRAPH) |
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   174
          command(TEXT) |
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   175
          command(TXT) |
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   176
          command(TEXT_RAW)) ~
69887
b9985133805d added semantic document markers;
wenzelm
parents: 69255
diff changeset
   177
        annotation ~! document_source
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58861
diff changeset
   178
69887
b9985133805d added semantic document markers;
wenzelm
parents: 69255
diff changeset
   179
      (rep(heading) ~ command(THEORY) ~ annotation) ~! args ^^ { case _ ~ x => x }
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   180
    }
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   181
  }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   182
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   183
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   184
  /* read -- lazy scanning */
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   185
65539
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   186
  private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) =
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   187
  {
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58908
diff changeset
   188
    val token = Token.Parsers.token(bootstrap_keywords)
64825
e78b62c289bb more uniform node_header (non-strict);
wenzelm
parents: 64824
diff changeset
   189
    def make_tokens(in: Reader[Char]): Stream[Token] =
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   190
      token(in) match {
64825
e78b62c289bb more uniform node_header (non-strict);
wenzelm
parents: 64824
diff changeset
   191
        case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
e78b62c289bb more uniform node_header (non-strict);
wenzelm
parents: 64824
diff changeset
   192
        case _ => Stream.empty
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   193
      }
64825
e78b62c289bb more uniform node_header (non-strict);
wenzelm
parents: 64824
diff changeset
   194
65539
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   195
    val all_tokens = make_tokens(reader)
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   196
    val drop_tokens =
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   197
      if (strict) Nil
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   198
      else all_tokens.takeWhile(tok => !tok.is_command(Thy_Header.THEORY)).toList
34190
dfcf667bbfed read header by scanning/parsing file;
wenzelm
parents: 34188
diff changeset
   199
65539
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   200
    val tokens = all_tokens.drop(drop_tokens.length)
64825
e78b62c289bb more uniform node_header (non-strict);
wenzelm
parents: 64824
diff changeset
   201
    val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList
e78b62c289bb more uniform node_header (non-strict);
wenzelm
parents: 64824
diff changeset
   202
    val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList
e78b62c289bb more uniform node_header (non-strict);
wenzelm
parents: 64824
diff changeset
   203
65539
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   204
    (drop_tokens, tokens1 ::: tokens2)
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   205
  }
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   206
68841
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   207
  private object Parser extends Parser
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   208
  {
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   209
    def parse_header(tokens: List[Token], pos: Token.Pos): Thy_Header =
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   210
      parse(commit(header), Token.reader(tokens, pos)) match {
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   211
        case Success(result, _) => result
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   212
        case bad => error(bad.toString)
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   213
      }
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   214
  }
252b43600737 clarified signature;
wenzelm
parents: 67722
diff changeset
   215
72775
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   216
  def read(node_name: Document.Node.Name, reader: Reader[Char],
72777
164cb0806d0a proper positions for inlined command messages, e.g. for completion within theory header;
wenzelm
parents: 72776
diff changeset
   217
    command: Boolean = true,
72774
51c0f79d6eed tuned signature;
wenzelm
parents: 72773
diff changeset
   218
    strict: Boolean = true): Thy_Header =
65539
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   219
  {
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   220
    val (_, tokens0) = read_tokens(reader, true)
66918
ec2b50aeb0dd more robust treatment of UTF8 in raw byte sources;
wenzelm
parents: 66713
diff changeset
   221
    val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
65539
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   222
72777
164cb0806d0a proper positions for inlined command messages, e.g. for completion within theory header;
wenzelm
parents: 72776
diff changeset
   223
    val (skip_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
164cb0806d0a proper positions for inlined command messages, e.g. for completion within theory header;
wenzelm
parents: 72776
diff changeset
   224
    val pos =
164cb0806d0a proper positions for inlined command messages, e.g. for completion within theory header;
wenzelm
parents: 72776
diff changeset
   225
      if (command) Token.Pos.command
164cb0806d0a proper positions for inlined command messages, e.g. for completion within theory header;
wenzelm
parents: 72776
diff changeset
   226
      else (Token.Pos.file(node_name.node) /: skip_tokens)(_ advance _)
65539
dbcd9b3e1b49 more precise position information;
wenzelm
parents: 65526
diff changeset
   227
72779
1cc74982d038 clarified parser;
wenzelm
parents: 72778
diff changeset
   228
    Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
34169
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   229
  }
7501b2910900 basic setup for header scanning/parsing;
wenzelm
parents: 32466
diff changeset
   230
}
44159
9a35e88d9dc9 simplified class Thy_Header;
wenzelm
parents: 44157
diff changeset
   231
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44163
diff changeset
   232
sealed case class Thy_Header(
72778
83e581c9a5f1 tuned signature;
wenzelm
parents: 72777
diff changeset
   233
  name: String,
83e581c9a5f1 tuned signature;
wenzelm
parents: 72777
diff changeset
   234
  pos: Position.T,
83e581c9a5f1 tuned signature;
wenzelm
parents: 72777
diff changeset
   235
  imports: List[(String, Position.T)],
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63449
diff changeset
   236
  keywords: Thy_Header.Keywords,
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63449
diff changeset
   237
  abbrevs: Thy_Header.Abbrevs)
70638
f164cec7ac22 clarified signature: prefer operations without position;
wenzelm
parents: 69887
diff changeset
   238
{
72764
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
   239
  def map(f: String => String): Thy_Header =
72778
83e581c9a5f1 tuned signature;
wenzelm
parents: 72777
diff changeset
   240
    Thy_Header(f(name), pos,
83e581c9a5f1 tuned signature;
wenzelm
parents: 72777
diff changeset
   241
      imports.map({ case (a, b) => (f(a), b) }),
72764
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
   242
      keywords.map({ case (a, spec) => (f(a), spec.map(f)) }),
722c0d02ffab clarified signature;
wenzelm
parents: 72748
diff changeset
   243
      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   244
72775
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   245
  def check(node_name: Document.Node.Name): Thy_Header =
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   246
  {
72775
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   247
    val base_name = node_name.theory_base_name
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   248
    if (Long_Name.is_qualified(name)) {
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   249
      error("Bad theory name " + quote(name) + " with qualification" + Position.here(pos))
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   250
    }
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   251
    if (base_name != name) {
72776
27a464537fb0 tuned signature;
wenzelm
parents: 72775
diff changeset
   252
      error("Bad theory name " + quote(name) + " for file " + Path.basic(base_name).thy +
27a464537fb0 tuned signature;
wenzelm
parents: 72775
diff changeset
   253
        Position.here(pos) + Completion.report_theories(pos, List(base_name)))
72775
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   254
    }
0a94eb91190d clarified modules;
wenzelm
parents: 72774
diff changeset
   255
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   256
    for ((_, spec) <- keywords) {
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   257
      if (spec.kind != Keyword.THY_LOAD && spec.load_command.nonEmpty) {
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   258
        error("Illegal load command specification for kind: " + quote(spec.kind) +
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   259
          Position.here(spec.kind_pos))
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   260
      }
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   261
      if (!Command_Span.load_commands.exists(_.name == spec.load_command)) {
72782
98ecb951d911 more completion;
wenzelm
parents: 72779
diff changeset
   262
        val completion =
98ecb951d911 more completion;
wenzelm
parents: 72779
diff changeset
   263
          for {
98ecb951d911 more completion;
wenzelm
parents: 72779
diff changeset
   264
            load_command <- Command_Span.load_commands
98ecb951d911 more completion;
wenzelm
parents: 72779
diff changeset
   265
            name = load_command.name
98ecb951d911 more completion;
wenzelm
parents: 72779
diff changeset
   266
            if name.startsWith(spec.load_command)
98ecb951d911 more completion;
wenzelm
parents: 72779
diff changeset
   267
          } yield (name, (Markup.LOAD_COMMAND, name))
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   268
        error("Unknown load command specification: " + quote(spec.load_command) +
72782
98ecb951d911 more completion;
wenzelm
parents: 72779
diff changeset
   269
          Position.here(spec.load_command_pos) +
98ecb951d911 more completion;
wenzelm
parents: 72779
diff changeset
   270
          Completion.report_names(spec.load_command_pos, completion))
72765
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   271
      }
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   272
    }
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   273
    this
f34f5c057c9e clarified parsing vs. semantic errors;
wenzelm
parents: 72764
diff changeset
   274
  }
70638
f164cec7ac22 clarified signature: prefer operations without position;
wenzelm
parents: 69887
diff changeset
   275
}