src/Pure/Thy/ROOT.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 74 208ab8773a73
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title:      Pure/Thy/ROOT
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Sonia Mahjoub / Tobias Nipkow
clasohm@0
     4
    Copyright   1992  TU Muenchen
clasohm@0
     5
clasohm@0
     6
This file builds the theory parser.
clasohm@0
     7
It assumes the standard Isabelle environment.
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
use "scan.ML";
clasohm@0
    11
use "parse.ML";
clasohm@0
    12
use "syntax.ML";
clasohm@0
    13
use "read.ML";
clasohm@0
    14
clasohm@0
    15
clasohm@0
    16
structure Keyword =
clasohm@0
    17
    struct
clasohm@0
    18
    val alphas =  ["classes", "default", "arities", "types",
clasohm@0
    19
                   "consts", "rules", "end", "rules", "mixfix",
clasohm@0
    20
                   "infixr", "infixl", "binder", "translations"]
clasohm@0
    21
clasohm@0
    22
    val symbols = [",", "<", "{", "}", "(", ")", "(*", "*)",
clasohm@0
    23
                   "[", "]", "::", "=", "+", "==", "=>", "<="]
clasohm@0
    24
    end;
clasohm@0
    25
clasohm@0
    26
structure Lex     = LexicalFUN (Keyword);
clasohm@0
    27
structure Parse   = ParseFUN (Lex);
clasohm@0
    28
structure ThySyn  = ThySynFUN (Parse);
clasohm@0
    29
structure Readthy = ReadthyFUN (ThySyn);
clasohm@0
    30
clasohm@0
    31
open Readthy;