src/Pure/Thy/thy_syn.ML
author paulson
Tue, 22 Jul 1997 11:14:18 +0200
changeset 3538 ed9de44032e0
parent 1512 ce37c64244c0
child 3619 0fc67ad6d62a
permissions -rw-r--r--
Removal of the tactical STATE
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
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     5
Interface for user syntax.
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_DATA =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
     9
  sig
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    10
  val user_keywords: string list
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    11
  val user_sections: (string * (ThyParse.token list -> (string * string)
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    12
    * ThyParse.token list)) list
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
    13
  end;
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    14
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    15
signature THY_SYN =
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
    16
  sig
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 411
diff changeset
    17
  val parse: string -> string -> string
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
    18
  end;
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    19
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
    20
functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    21
struct
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    22
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
    23
val syntax =
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
    24
  ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
    25
		       (ThyParse.pure_sections @ Data.user_sections);
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    26
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 476
diff changeset
    27
val parse = ThyParse.parse_thy syntax;
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    28
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    29
end;
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    30