src/Pure/Thy/thy_header.ML
author wenzelm
Thu Nov 02 10:16:22 2017 +0100 (20 months ago)
changeset 66987 352b23c97ac8
parent 66771 925d10a7a610
child 67013 335a7dce7cb3
permissions -rw-r--r--
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
     1 (*  Title:      Pure/Thy/thy_header.ML
     2     Author:     Makarius
     3 
     4 Static theory header information.
     5 *)
     6 
     7 signature THY_HEADER =
     8 sig
     9   type keywords = ((string * Position.T) * Keyword.spec) list
    10   type header =
    11    {name: string * Position.T,
    12     imports: (string * Position.T) list,
    13     keywords: keywords}
    14   val make: string * Position.T -> (string * Position.T) list -> keywords -> header
    15   val theoryN: string
    16   val bootstrap_keywords: Keyword.keywords
    17   val add_keywords: keywords -> theory -> theory
    18   val get_keywords: theory -> Keyword.keywords
    19   val get_keywords': Proof.context -> Keyword.keywords
    20   val ml_bootstrapN: string
    21   val ml_roots: string list
    22   val bootstrap_thys: string list
    23   val is_base_name: string -> bool
    24   val import_name: string -> string
    25   val args: header parser
    26   val read: Position.T -> string -> header
    27   val read_tokens: Token.T list -> header
    28 end;
    29 
    30 structure Thy_Header: THY_HEADER =
    31 struct
    32 
    33 (** keyword declarations **)
    34 
    35 (* header *)
    36 
    37 type keywords = ((string * Position.T) * Keyword.spec) list;
    38 
    39 type header =
    40  {name: string * Position.T,
    41   imports: (string * Position.T) list,
    42   keywords: keywords};
    43 
    44 fun make name imports keywords : header =
    45   {name = name, imports = imports, keywords = keywords};
    46 
    47 
    48 (* bootstrap keywords *)
    49 
    50 val chapterN = "chapter";
    51 val sectionN = "section";
    52 val subsectionN = "subsection";
    53 val subsubsectionN = "subsubsection";
    54 val paragraphN = "paragraph";
    55 val subparagraphN = "subparagraph";
    56 val textN = "text";
    57 val txtN = "txt";
    58 val text_rawN = "text_raw";
    59 
    60 val theoryN = "theory";
    61 val importsN = "imports";
    62 val keywordsN = "keywords";
    63 val abbrevsN = "abbrevs";
    64 val beginN = "begin";
    65 
    66 val bootstrap_keywords =
    67   Keyword.empty_keywords
    68   |> Keyword.add_keywords
    69     [(("%", \<^here>), Keyword.no_spec),
    70      (("(", \<^here>), Keyword.no_spec),
    71      ((")", \<^here>), Keyword.no_spec),
    72      ((",", \<^here>), Keyword.no_spec),
    73      (("::", \<^here>), Keyword.no_spec),
    74      (("=", \<^here>), Keyword.no_spec),
    75      (("and", \<^here>), Keyword.no_spec),
    76      ((beginN, \<^here>), Keyword.quasi_command_spec),
    77      ((importsN, \<^here>), Keyword.quasi_command_spec),
    78      ((keywordsN, \<^here>), Keyword.quasi_command_spec),
    79      ((abbrevsN, \<^here>), Keyword.quasi_command_spec),
    80      ((chapterN, \<^here>), ((Keyword.document_heading, []), [])),
    81      ((sectionN, \<^here>), ((Keyword.document_heading, []), [])),
    82      ((subsectionN, \<^here>), ((Keyword.document_heading, []), [])),
    83      ((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])),
    84      ((paragraphN, \<^here>), ((Keyword.document_heading, []), [])),
    85      ((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])),
    86      ((textN, \<^here>), ((Keyword.document_body, []), [])),
    87      ((txtN, \<^here>), ((Keyword.document_body, []), [])),
    88      ((text_rawN, \<^here>), ((Keyword.document_raw, []), [])),
    89      ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
    90      (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];
    91 
    92 
    93 (* theory data *)
    94 
    95 structure Data = Theory_Data
    96 (
    97   type T = Keyword.keywords;
    98   val empty = bootstrap_keywords;
    99   val extend = I;
   100   val merge = Keyword.merge_keywords;
   101 );
   102 
   103 val add_keywords = Data.map o Keyword.add_keywords;
   104 
   105 val get_keywords = Data.get;
   106 val get_keywords' = get_keywords o Proof_Context.theory_of;
   107 
   108 
   109 
   110 (** concrete syntax **)
   111 
   112 (* names *)
   113 
   114 val ml_bootstrapN = "ML_Bootstrap";
   115 val ml_roots = ["ML_Root0", "ML_Root"];
   116 val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
   117 
   118 fun is_base_name s =
   119   s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s)
   120 
   121 val import_name = Path.base_name o Path.explode;
   122 
   123 
   124 (* header args *)
   125 
   126 local
   127 
   128 fun imports name =
   129   if name = Context.PureN then Scan.succeed []
   130   else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name));
   131 
   132 val opt_files =
   133   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
   134 
   135 val keyword_spec =
   136   Parse.group (fn () => "outer syntax keyword specification")
   137     (Parse.name -- opt_files -- Parse.tags);
   138 
   139 val keyword_decl =
   140   Scan.repeat1 (Parse.position Parse.string) --
   141   Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
   142   >> (fn (names, spec) => map (rpair spec) names);
   143 
   144 val abbrevs = Scan.repeat1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
   145 
   146 val keyword_decls = Parse.and_list1 keyword_decl >> flat;
   147 
   148 in
   149 
   150 val args =
   151   Parse.position Parse.theory_name :|-- (fn (name, pos) =>
   152     imports name --
   153     Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
   154     (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN)
   155     >> (fn (imports, keywords) => make (name, pos) imports keywords));
   156 
   157 end;
   158 
   159 
   160 (* read header *)
   161 
   162 val heading =
   163   (Parse.command chapterN ||
   164     Parse.command sectionN ||
   165     Parse.command subsectionN ||
   166     Parse.command subsubsectionN ||
   167     Parse.command paragraphN ||
   168     Parse.command subparagraphN ||
   169     Parse.command textN ||
   170     Parse.command txtN ||
   171     Parse.command text_rawN) --
   172   Parse.tags -- Parse.!!! Parse.document_source;
   173 
   174 val header =
   175   (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
   176 
   177 fun token_source pos =
   178   Symbol.explode
   179   #> Source.of_list
   180   #> Token.source_strict bootstrap_keywords pos;
   181 
   182 fun read_source pos source =
   183   let val res =
   184     source
   185     |> Token.source_proper
   186     |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header)))
   187     |> Source.get_single;
   188   in
   189     (case res of
   190       SOME (h, _) => h
   191     | NONE => error ("Unexpected end of input" ^ Position.here pos))
   192   end;
   193 
   194 fun read pos str = read_source pos (token_source pos str);
   195 fun read_tokens toks = read_source Position.none (Source.of_list toks);
   196 
   197 end;