src/Pure/Thy/ROOT.ML
author wenzelm
Wed Jun 01 15:47:27 1994 +0200 (1994-06-01)
changeset 413 2a1554524ad5
parent 390 b074205ac50a
child 431 da3d07d4349b
permissions -rw-r--r--
removed garbage;
adapted to new ThySyn (interface for 'user sections');
wenzelm@390
     1
(*  Title:      Pure/Thy/ROOT.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@390
     3
    Author:     Sonia Mahjoub and Tobias Nipkow and
wenzelm@390
     4
                Markus Wenzel and Carsten Clasohm, TU Muenchen
clasohm@0
     5
wenzelm@390
     6
This file builds the theory parser and autoloading system.
clasohm@0
     7
*)
clasohm@0
     8
wenzelm@390
     9
(* FIXME remove (still needed by HOL/Datatype.ML) *)
wenzelm@390
    10
use "scan.ML"; use "parse.ML";
wenzelm@390
    11
wenzelm@413
    12
wenzelm@390
    13
use "thy_scan.ML";
wenzelm@390
    14
use "thy_parse.ML";
wenzelm@390
    15
wenzelm@390
    16
structure ThyScan = ThyScanFun(Scanner);
wenzelm@390
    17
structure ThyParse = ThyParseFun(structure Symtab = Symtab
wenzelm@390
    18
  and ThyScan = ThyScan);
clasohm@0
    19
wenzelm@413
    20
use "thy_syn.ML";
wenzelm@413
    21
use "thy_read.ML";
clasohm@0
    22
wenzelm@413
    23
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
wenzelm@413
    24
structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);
wenzelm@413
    25
open Readthy;
clasohm@0
    26
wenzelm@413
    27
fun init_thy_reader () =
wenzelm@413
    28
  use_string
wenzelm@413
    29
   ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);",
wenzelm@413
    30
    "Readthy.loaded_thys := ! loaded_thys;",
wenzelm@413
    31
    "open Readthy;"];
clasohm@74
    32