src/Pure/Thy/thy_syn.ML
author wenzelm
Wed, 06 Aug 1997 11:52:16 +0200
changeset 3619 0fc67ad6d62a
parent 1512 ce37c64244c0
child 3620 ed1416badb41
permissions -rw-r--r--
eliminated ThySynData and ThySynFun; added ThySyn.add_syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thy_syn.ML
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     4
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
     5
Syntax for thy files.
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     6
*)
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     7
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     8
signature THY_SYN =
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
     9
sig
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    10
  val add_syntax: string list ->
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    11
    (string * (ThyParse.token list -> (string * string) * ThyParse.token list)) list
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    12
    -> unit
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 411
diff changeset
    13
  val parse: string -> string -> string
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    14
end;
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    15
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    16
structure ThySyn: THY_SYN =
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    17
struct
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    18
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    19
(* current syntax *)
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    20
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    21
val keywords = ref ThyParse.pure_keywords;
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    22
val sections = ref ThyParse.pure_sections;
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    23
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    24
fun make_syntax () =
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    25
  ThyParse.make_syntax (! keywords) (!sections);
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    26
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    27
val syntax = ref (make_syntax ());
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    28
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    29
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    30
(* augment syntax *)
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    31
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    32
fun add_syntax keys sects =
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    33
 (keywords := keys union ! keywords;
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    34
  sections := sects @ ! sections;
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    35
  syntax := make_syntax ());
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    36
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    37
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    38
(* parse *)
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    39
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    40
fun parse name txt =
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    41
  ThyParse.parse_thy (! syntax) name txt;
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    42
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    43
end;