src/Pure/Thy/thy_syn.ML
author wenzelm
Fri, 16 Jul 1999 22:24:42 +0200
changeset 7024 44bd3c094fd6
parent 6641 254ab03bd082
child 11819 9283b3c11234
permissions -rw-r--r--
tuned;
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
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
     5
Provide syntax for old-style theory files.
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     6
*)
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
     7
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
     8
signature BASIC_THY_SYN =
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
     9
sig
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    10
  val delete_tmpfiles: bool ref
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    11
end;
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    12
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    13
signature THY_SYN =
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    14
sig
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    15
  include BASIC_THY_SYN
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    16
  val add_syntax: string list ->
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    17
    (string * (ThyParse.token list -> (string * string) * ThyParse.token list)) list
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    18
    -> unit
7024
wenzelm
parents: 6641
diff changeset
    19
  val get_lexicon: unit -> Scan.lexicon
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    20
  val load_thy: string -> string list -> unit
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    21
end;
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    22
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    23
structure ThySyn: THY_SYN =
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    24
struct
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    25
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    26
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    27
(* current syntax *)
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    28
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    29
val keywords = ref ThyParse.pure_keywords;
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    30
val sections = ref ThyParse.pure_sections;
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    31
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    32
fun make_syntax () =
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    33
  ThyParse.make_syntax (! keywords) (!sections);
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    34
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    35
val syntax = ref (make_syntax ());
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    36
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    37
fun get_lexicon () = ThyParse.get_lexicon (! syntax);
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    38
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    39
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    40
(* augment syntax *)
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    41
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    42
fun add_syntax keys sects =
3620
wenzelm
parents: 3619
diff changeset
    43
 (keywords := (keys union ! keywords);
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    44
  sections := sects @ ! sections;
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    45
  syntax := make_syntax ());
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    46
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    47
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    48
(* load_thy *)
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    49
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    50
val delete_tmpfiles = ref true;
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 1512
diff changeset
    51
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    52
fun load_thy name chs =
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    53
  let
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    54
    val tmp_path = File.tmp_path (ThyLoad.ml_path (name ^ "_thy"));
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    55
    val txt_out = ThyParse.parse_thy (! syntax) chs;
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    56
  in
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    57
    File.write tmp_path txt_out;
6641
254ab03bd082 rearranged some modules;
wenzelm
parents: 6231
diff changeset
    58
    File.symbol_use tmp_path;
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    59
    if ! delete_tmpfiles then File.rm tmp_path else ()
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    60
  end;
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    61
411
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    62
4860901706db interface for 'user sections';
wenzelm
parents:
diff changeset
    63
end;
6206
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    64
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    65
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    66
structure BasicThySyn: BASIC_THY_SYN = ThySyn;
7d2204fcc1e5 delete_tmpfiles (from thy_read.ML);
wenzelm
parents: 3620
diff changeset
    67
open BasicThySyn;