--- a/src/Pure/Thy/ROOT.ML Wed Aug 06 11:19:59 1997 +0200
+++ b/src/Pure/Thy/ROOT.ML Wed Aug 06 11:52:16 1997 +0200
@@ -9,16 +9,16 @@
use "thy_scan.ML";
use "thy_parse.ML";
use "thy_syn.ML";
+
use "thy_info.ML";
use "browser_info.ML";
use "thm_database.ML";
+
use "symbol_input.ML";
use "thy_read.ML";
-open ThmDB ReadThy ThyInfo BrowserInfo SymbolInput;
+open ThmDB ThyRead ThyInfo BrowserInfo SymbolInput;
-structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
-set_parser ThySyn.parse;
(* FIXME tmp *)
--- a/src/Pure/Thy/thy_read.ML Wed Aug 06 11:19:59 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML Wed Aug 06 11:52:16 1997 +0200
@@ -7,7 +7,7 @@
Functions for reading theory files.
*)
-signature READTHY =
+signature THY_READ =
sig
datatype basetype = Thy of string
| File of string
@@ -15,8 +15,6 @@
val loadpath : string list ref
val delete_tmpfiles: bool ref
- val set_parser : (string -> string -> string) -> unit
-
val use_thy : string -> unit
val time_use_thy : string -> unit
val use_dir : string -> unit
@@ -27,7 +25,7 @@
end;
-structure ReadThy : READTHY =
+structure ThyRead: THY_READ =
struct
open ThmDB ThyInfo BrowserInfo;
@@ -37,14 +35,6 @@
| File of string;
-(*parser for theory files*)
-val parser = ref ((K (K "")):string -> string -> string);
-
-
-(*set parser for theory files*)
-fun set_parser p = parser := p;
-
-
(*Default search path for theory files*)
val loadpath = ref ["."];
@@ -66,12 +56,13 @@
fun read_thy tname thy_file =
let
val instream = TextIO.openIn thy_file;
+ val intext = TextIO.inputAll instream;
+ val _ = TextIO.closeIn instream;
+ val outext = ThySyn.parse tname intext;
val outstream = TextIO.openOut (out_name tname);
- in
- TextIO.output (outstream, (!parser) tname (TextIO.inputAll instream));
- TextIO.closeOut outstream;
- TextIO.closeIn instream
- end;
+ val _ = TextIO.output (outstream, outext);
+ val _ = TextIO.closeOut outstream;
+ in () end;
(*Check if a theory was completly loaded *)
--- a/src/Pure/Thy/thy_syn.ML Wed Aug 06 11:19:59 1997 +0200
+++ b/src/Pure/Thy/thy_syn.ML Wed Aug 06 11:52:16 1997 +0200
@@ -2,29 +2,42 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Interface for user syntax.
+Syntax for thy files.
*)
-signature THY_SYN_DATA =
- sig
- val user_keywords: string list
- val user_sections: (string * (ThyParse.token list -> (string * string)
- * ThyParse.token list)) list
- end;
-
signature THY_SYN =
- sig
+sig
+ val add_syntax: string list ->
+ (string * (ThyParse.token list -> (string * string) * ThyParse.token list)) list
+ -> unit
val parse: string -> string -> string
- end;
+end;
-functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
+structure ThySyn: THY_SYN =
struct
-val syntax =
- ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
- (ThyParse.pure_sections @ Data.user_sections);
+(* current syntax *)
+
+val keywords = ref ThyParse.pure_keywords;
+val sections = ref ThyParse.pure_sections;
+
+fun make_syntax () =
+ ThyParse.make_syntax (! keywords) (!sections);
+
+val syntax = ref (make_syntax ());
+
-val parse = ThyParse.parse_thy syntax;
+(* augment syntax *)
+
+fun add_syntax keys sects =
+ (keywords := keys union ! keywords;
+ sections := sects @ ! sections;
+ syntax := make_syntax ());
+
+
+(* parse *)
+
+fun parse name txt =
+ ThyParse.parse_thy (! syntax) name txt;
end;
-