get_lexicon;
authorwenzelm
Wed Feb 03 17:28:02 1999 +0100 (1999-02-03)
changeset 6208ea009b75b74e
parent 6207 58e9f980bd4f
child 6209 7059f46603e2
get_lexicon;
parse_thy: eliminated name, get exploded text;
simplified header handling;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Feb 03 17:26:53 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Feb 03 17:28:02 1999 +0100
     1.3 @@ -48,9 +48,10 @@
     1.4    val opt_witness: token list -> string * token list
     1.5    val const_decls: token list -> string * token list
     1.6    type syntax
     1.7 +  val get_lexicon: syntax -> Scan.lexicon;
     1.8    val make_syntax: string list ->
     1.9      (string * (token list -> (string * string) * token list)) list -> syntax
    1.10 -  val parse_thy: syntax -> string -> string -> string
    1.11 +  val parse_thy: syntax -> string list -> string
    1.12    val section: string -> string -> (token list -> string * token list)
    1.13      -> (string * (token list -> (string * string) * token list))
    1.14    val axm_section: string -> string
    1.15 @@ -446,6 +447,8 @@
    1.16  type syntax =
    1.17    Scan.lexicon * (token list -> (string * string) * token list) Symtab.table;
    1.18  
    1.19 +fun get_lexicon (lex, _) = lex;
    1.20 +
    1.21  fun make_syntax keywords sects =
    1.22    let
    1.23      val dups = duplicates (map fst sects);
    1.24 @@ -460,14 +463,10 @@
    1.25  
    1.26  (* header *)
    1.27  
    1.28 -fun mk_header (thy_name, bases) =
    1.29 -  (thy_name, "mk_base " ^ mk_list bases ^ " " ^ quote thy_name);
    1.30 +fun mk_header (thy_name, parents) =
    1.31 +  (thy_name, "ThyInfo.begin_theory " ^ cat (quote thy_name) (mk_list parents));
    1.32  
    1.33 -val base =
    1.34 -  ident >> (cat "Thy" o quote) ||
    1.35 -  string >> cat "File";
    1.36 -
    1.37 -val header = ident --$$ "=" -- enum1 "+" base >> mk_header;
    1.38 +val header = ident --$$ "=" -- enum1 "+" name >> mk_header;
    1.39  
    1.40  
    1.41  (* extension *)
    1.42 @@ -496,50 +495,41 @@
    1.43  
    1.44  (* theory definition *)
    1.45  
    1.46 -fun mk_structure tname ((thy_name, old_thys), (extxt, postxt, mltxt)) =
    1.47 -  if thy_name <> tname then
    1.48 -    error ("Filename \"" ^ tname ^ ".thy\" and theory name "
    1.49 -      ^ quote thy_name ^ " are different")
    1.50 -  else
    1.51 -    "val thy = " ^ old_thys ^ ";\n\n\
    1.52 -    \structure " ^ thy_name ^ " =\n\
    1.53 -    \struct\n\
    1.54 -    \\n\
    1.55 -    \local\n"
    1.56 -    ^ local_defs ^ "\n\
    1.57 -    \in\n\
    1.58 -    \\n"
    1.59 -    ^ mltxt ^ "\n\
    1.60 -    \\n\
    1.61 -    \val thy = thy\n\
    1.62 -    \|> PureThy.put_name " ^ quote thy_name ^ "\n\
    1.63 -    \|> PureThy.local_path\n\
    1.64 -    \|> Theory.add_trfuns\n"
    1.65 -    ^ trfun_args ^ "\n\
    1.66 -    \|> Theory.add_trfunsT typed_print_translation\n\
    1.67 -    \|> Theory.add_tokentrfuns token_translation\n\
    1.68 -    \\n"
    1.69 -    ^ extxt ^ "\n\
    1.70 -    \\n\
    1.71 -    \|> PureThy.end_theory\n\
    1.72 -    \\n\
    1.73 -    \val _ = store_theory thy;\n\
    1.74 -    \val _ = context thy;\n\
    1.75 -    \\n\
    1.76 -    \\n"
    1.77 -    ^ postxt ^ "\n\
    1.78 -    \\n\
    1.79 -    \end;\n\
    1.80 -    \end;\n\
    1.81 -    \\n\
    1.82 -    \open " ^ thy_name ^ ";\n\
    1.83 -    \\n";
    1.84 +fun mk_structure ((thy_name, bg_theory), (extxt, postxt, mltxt)) =
    1.85 +  "structure " ^ thy_name ^ " =\n\
    1.86 +  \struct\n\
    1.87 +  \\n\
    1.88 +  \local\n"
    1.89 +  ^ local_defs ^ "\n\
    1.90 +  \in\n\
    1.91 +  \\n"
    1.92 +  ^ mltxt ^ "\n\
    1.93 +  \\n\
    1.94 +  \val thy = " ^ bg_theory ^ "\n\
    1.95 +  \\n\
    1.96 +  \|> Theory.add_trfuns\n"
    1.97 +  ^ trfun_args ^ "\n\
    1.98 +  \|> Theory.add_trfunsT typed_print_translation\n\
    1.99 +  \|> Theory.add_tokentrfuns token_translation\n\
   1.100 +  \\n"
   1.101 +  ^ extxt ^ "\n\
   1.102 +  \\n\
   1.103 +  \|> ThyInfo.end_theory;\n\
   1.104 +  \\n\
   1.105 +  \val _ = context thy;\n\
   1.106 +  \\n\
   1.107 +  \\n"
   1.108 +  ^ postxt ^ "\n\
   1.109 +  \\n\
   1.110 +  \end;\n\
   1.111 +  \end;\n\
   1.112 +  \\n\
   1.113 +  \open " ^ thy_name ^ ";\n";
   1.114  
   1.115 -fun theory_defn sectab tname =
   1.116 -  header -- opt_extension sectab -- eof >> (mk_structure tname o #1);
   1.117 +fun theory_defn sectab =
   1.118 +  header -- opt_extension sectab -- eof >> (mk_structure o #1);
   1.119  
   1.120 -fun parse_thy (lex, sectab) tname str =
   1.121 -  #1 (!! (theory_defn sectab tname) (tokenize lex str));
   1.122 +fun parse_thy (lex, sectab) chs = #1 (!! (theory_defn sectab) (tokenize lex chs));
   1.123  
   1.124  
   1.125  (* standard sections *)