src/Tools/code/code_target.ML
changeset 28663 bd8438543bf2
parent 28090 29af3c712d2b
child 28690 fc51fa5efea1
     1.1 --- a/src/Tools/code/code_target.ML	Wed Oct 22 14:15:44 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Wed Oct 22 14:15:45 2008 +0200
     1.3 @@ -11,7 +11,8 @@
     1.4  
     1.5    type serializer
     1.6    val add_target: string * (serializer * literals) -> theory -> theory
     1.7 -  val extend_target: string * (string * (Code_Thingol.program -> Code_Thingol.program))
     1.8 +  val extend_target: string *
     1.9 +      (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    1.10      -> theory -> theory
    1.11    val assert_target: theory -> string -> string
    1.12  
    1.13 @@ -24,20 +25,18 @@
    1.14    val code_writeln: Pretty.T -> unit
    1.15    val mk_serialization: string -> ('a -> unit) option
    1.16      -> (Path.T option -> 'a -> unit)
    1.17 -    -> ('a -> string * string list)
    1.18 +    -> ('a -> string * string option list)
    1.19      -> 'a -> serialization
    1.20    val serialize: theory -> string -> string option -> Args.T list
    1.21 -    -> Code_Thingol.program -> string list -> serialization
    1.22 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    1.23    val serialize_custom: theory -> string * (serializer * literals)
    1.24 -    -> Code_Thingol.program -> string list -> string * string list
    1.25 +    -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    1.26    val the_literals: theory -> string -> literals
    1.27    val compile: serialization -> unit
    1.28    val export: serialization -> unit
    1.29    val file: Path.T -> serialization -> unit
    1.30    val string: string list -> serialization -> string
    1.31 -
    1.32    val code_of: theory -> string -> string -> string list -> string list -> string
    1.33 -  val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    1.34    val code_width: int ref
    1.35  
    1.36    val allow_abort: string -> theory -> theory
    1.37 @@ -45,11 +44,7 @@
    1.38      -> (string * (string * string) list) option -> theory -> theory
    1.39    val add_syntax_inst: string -> string * class -> bool -> theory -> theory
    1.40    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    1.41 -  val add_syntax_tycoP: string -> string -> OuterParse.token list
    1.42 -    -> (theory -> theory) * OuterParse.token list
    1.43    val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
    1.44 -  val add_syntax_constP: string -> string -> OuterParse.token list
    1.45 -    -> (theory -> theory) * OuterParse.token list
    1.46    val add_reserved: string -> string -> theory -> theory
    1.47  end;
    1.48  
    1.49 @@ -62,7 +57,7 @@
    1.50  (** basics **)
    1.51  
    1.52  datatype destination = Compile | Export | File of Path.T | String of string list;
    1.53 -type serialization = destination -> (string * string list) option;
    1.54 +type serialization = destination -> (string * string option list) option;
    1.55  
    1.56  val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
    1.57  fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
    1.58 @@ -87,22 +82,24 @@
    1.59  
    1.60  (** theory data **)
    1.61  
    1.62 +structure StringPairTab = Code_Name.StringPairTab;
    1.63 +
    1.64  datatype name_syntax_table = NameSyntaxTable of {
    1.65    class: class_syntax Symtab.table,
    1.66 -  inst: unit Symtab.table,
    1.67 +  instance: unit StringPairTab.table,
    1.68    tyco: tyco_syntax Symtab.table,
    1.69    const: const_syntax Symtab.table
    1.70  };
    1.71  
    1.72 -fun mk_name_syntax_table ((class, inst), (tyco, const)) =
    1.73 -  NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
    1.74 -fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
    1.75 -  mk_name_syntax_table (f ((class, inst), (tyco, const)));
    1.76 -fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
    1.77 -    NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
    1.78 +fun mk_name_syntax_table ((class, instance), (tyco, const)) =
    1.79 +  NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
    1.80 +fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
    1.81 +  mk_name_syntax_table (f ((class, instance), (tyco, const)));
    1.82 +fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
    1.83 +    NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
    1.84    mk_name_syntax_table (
    1.85      (Symtab.join (K snd) (class1, class2),
    1.86 -       Symtab.join (K snd) (inst1, inst2)),
    1.87 +       StringPairTab.join (K snd) (instance1, instance2)),
    1.88      (Symtab.join (K snd) (tyco1, tyco2),
    1.89         Symtab.join (K snd) (const1, const2))
    1.90    );
    1.91 @@ -117,12 +114,13 @@
    1.92    -> (string -> class_syntax option)
    1.93    -> (string -> tyco_syntax option)
    1.94    -> (string -> const_syntax option)
    1.95 +  -> Code_Thingol.naming
    1.96    -> Code_Thingol.program
    1.97    -> string list                        (*selected statements*)
    1.98    -> serialization;
    1.99  
   1.100  datatype serializer_entry = Serializer of serializer * literals
   1.101 -  | Extends of string * (Code_Thingol.program -> Code_Thingol.program);
   1.102 +  | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
   1.103  
   1.104  datatype target = Target of {
   1.105    serial: serial,
   1.106 @@ -178,19 +176,25 @@
   1.107  
   1.108  fun put_target (target, seri) thy =
   1.109    let
   1.110 -    val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
   1.111 +    val lookup_target = Symtab.lookup (fst (CodeTargetData.get thy));
   1.112      val _ = case seri
   1.113 -     of Extends (super, _) => if defined_target super then ()
   1.114 +     of Extends (super, _) => if is_some (lookup_target super) then ()
   1.115            else error ("Unknown code target language: " ^ quote super)
   1.116        | _ => ();
   1.117 -    val _ = if defined_target target
   1.118 +    val overwriting = case (Option.map the_serializer o lookup_target) target
   1.119 +     of NONE => false
   1.120 +      | SOME (Extends _) => true
   1.121 +      | SOME (Serializer _) => (case seri
   1.122 +         of Extends _ => error ("Will not overwrite existing target " ^ quote target)
   1.123 +          | _ => true);
   1.124 +    val _ = if overwriting
   1.125        then warning ("Overwriting existing target " ^ quote target)
   1.126 -      else ();
   1.127 +      else (); 
   1.128    in
   1.129      thy
   1.130      |> (CodeTargetData.map o apfst oo Symtab.map_default)
   1.131            (target, mk_target ((serial (), seri), (([], Symtab.empty),
   1.132 -            (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
   1.133 +            (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)),
   1.134                Symtab.empty))))
   1.135            ((map_target o apfst o apsnd o K) seri)
   1.136    end;
   1.137 @@ -241,9 +245,8 @@
   1.138  fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
   1.139    let
   1.140      val class = prep_class thy raw_class;
   1.141 -    val class' = Code_Name.class thy class;
   1.142      fun mk_classparam c = case AxClass.class_of_param thy c
   1.143 -     of SOME class'' => if class = class'' then Code_Name.const thy c
   1.144 +     of SOME class' => if class = class' then c
   1.145            else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
   1.146        | NONE => error ("Not a class operation: " ^ quote c);
   1.147      fun mk_syntax_params raw_params = AList.lookup (op =)
   1.148 @@ -252,30 +255,29 @@
   1.149     of SOME (syntax, raw_params) =>
   1.150        thy
   1.151        |> (map_name_syntax target o apfst o apfst)
   1.152 -           (Symtab.update (class', (syntax, mk_syntax_params raw_params)))
   1.153 +           (Symtab.update (class, (syntax, mk_syntax_params raw_params)))
   1.154      | NONE =>
   1.155        thy
   1.156        |> (map_name_syntax target o apfst o apfst)
   1.157 -           (Symtab.delete_safe class')
   1.158 +           (Symtab.delete_safe class)
   1.159    end;
   1.160  
   1.161  fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
   1.162    let
   1.163 -    val inst = Code_Name.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
   1.164 +    val inst = (prep_class thy raw_class, prep_tyco thy raw_tyco);
   1.165    in if add_del then
   1.166      thy
   1.167      |> (map_name_syntax target o apfst o apsnd)
   1.168 -        (Symtab.update (inst, ()))
   1.169 +        (StringPairTab.update (inst, ()))
   1.170    else
   1.171      thy
   1.172      |> (map_name_syntax target o apfst o apsnd)
   1.173 -        (Symtab.delete_safe inst)
   1.174 +        (StringPairTab.delete_safe inst)
   1.175    end;
   1.176  
   1.177  fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
   1.178    let
   1.179      val tyco = prep_tyco thy raw_tyco;
   1.180 -    val tyco' = if tyco = "fun" then "fun" else Code_Name.tyco thy tyco;
   1.181      fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
   1.182        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   1.183        else syntax
   1.184 @@ -283,17 +285,16 @@
   1.185     of SOME syntax =>
   1.186        thy
   1.187        |> (map_name_syntax target o apsnd o apfst)
   1.188 -           (Symtab.update (tyco', check_args syntax))
   1.189 +           (Symtab.update (tyco, check_args syntax))
   1.190     | NONE =>
   1.191        thy
   1.192        |> (map_name_syntax target o apsnd o apfst)
   1.193 -           (Symtab.delete_safe tyco')
   1.194 +           (Symtab.delete_safe tyco)
   1.195    end;
   1.196  
   1.197  fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
   1.198    let
   1.199      val c = prep_const thy raw_c;
   1.200 -    val c' = Code_Name.const thy c;
   1.201      fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c
   1.202        then error ("Too many arguments in syntax for constant " ^ quote c)
   1.203        else syntax;
   1.204 @@ -301,11 +302,11 @@
   1.205     of SOME syntax =>
   1.206        thy
   1.207        |> (map_name_syntax target o apsnd o apsnd)
   1.208 -           (Symtab.update (c', check_args syntax))
   1.209 +           (Symtab.update (c, check_args syntax))
   1.210     | NONE =>
   1.211        thy
   1.212        |> (map_name_syntax target o apsnd o apsnd)
   1.213 -           (Symtab.delete_safe c')
   1.214 +           (Symtab.delete_safe c)
   1.215    end;
   1.216  
   1.217  fun add_reserved target =
   1.218 @@ -330,11 +331,10 @@
   1.219  fun add_module_alias target =
   1.220    map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename;
   1.221  
   1.222 -fun gen_allow_abort prep_cs raw_c thy =
   1.223 +fun gen_allow_abort prep_const raw_c thy =
   1.224    let
   1.225 -    val c = prep_cs thy raw_c;
   1.226 -    val c' = Code_Name.const thy c;
   1.227 -  in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
   1.228 +    val c = prep_const thy raw_c;
   1.229 +  in thy |> (CodeTargetData.map o apsnd) (insert (op =) c) end;
   1.230  
   1.231  fun zip_list (x::xs) f g =
   1.232    f
   1.233 @@ -355,8 +355,6 @@
   1.234  
   1.235  in
   1.236  
   1.237 -val parse_syntax = parse_syntax;
   1.238 -
   1.239  val add_syntax_class = gen_add_syntax_class cert_class (K I);
   1.240  val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
   1.241  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
   1.242 @@ -370,11 +368,6 @@
   1.243  val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const;
   1.244  val allow_abort_cmd = gen_allow_abort Code_Unit.read_const;
   1.245  
   1.246 -fun add_syntax_tycoP target tyco = parse_syntax I
   1.247 -  >> add_syntax_tyco_cmd target tyco;
   1.248 -fun add_syntax_constP target c = parse_syntax fst
   1.249 -  >> (add_syntax_const_cmd target c o Code_Printer.simple_const_syntax);
   1.250 -
   1.251  fun the_literals thy =
   1.252    let
   1.253      val (targets, _) = CodeTargetData.get thy;
   1.254 @@ -390,27 +383,63 @@
   1.255  
   1.256  (* montage *)
   1.257  
   1.258 -fun invoke_serializer thy modify abortable serializer reserved includes 
   1.259 -    module_alias class inst tyco const module args program1 cs1 =
   1.260 +local
   1.261 +
   1.262 +fun labelled_name thy program name = case Graph.get_node program name
   1.263 + of Code_Thingol.Fun (c, _) => quote (Code_Unit.string_of_const thy c)
   1.264 +  | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
   1.265 +  | Code_Thingol.Datatypecons (c, _) => quote (Code_Unit.string_of_const thy c)
   1.266 +  | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
   1.267 +  | Code_Thingol.Classrel (sub, super) => let
   1.268 +        val Code_Thingol.Class (sub, _) = Graph.get_node program sub
   1.269 +        val Code_Thingol.Class (super, _) = Graph.get_node program super
   1.270 +      in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
   1.271 +  | Code_Thingol.Classparam (c, _) => quote (Code_Unit.string_of_const thy c)
   1.272 +  | Code_Thingol.Classinst ((class, (tyco, _)), _) => let
   1.273 +        val Code_Thingol.Class (class, _) = Graph.get_node program class
   1.274 +        val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
   1.275 +      in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
   1.276 +
   1.277 +fun invoke_serializer thy abortable serializer reserved includes 
   1.278 +    module_alias class instance tyco const module args naming program2 names1 =
   1.279    let
   1.280 -    val program2 = modify program1;
   1.281 -    val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
   1.282 -    val cs2 = subtract (op =) hidden cs1;
   1.283 -    val program3 = Graph.subgraph (not o member (op =) hidden) program2;
   1.284 -    val all_cs = Graph.all_succs program2 cs2;
   1.285 -    val program4 = Graph.subgraph (member (op =) all_cs) program3;
   1.286 +    fun distill_names lookup_name src_tab = Symtab.empty
   1.287 +      |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier
   1.288 +           of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
   1.289 +            | NONE => (NONE, tab)) (Symtab.keys src_tab)
   1.290 +      |>> map_filter I;
   1.291 +    fun lookup_classparam_rev c' = case try (Graph.get_node program2) c'
   1.292 +     of SOME (Code_Thingol.Classparam (c, _)) => SOME c
   1.293 +      | NONE => NONE;
   1.294 +    fun lookup_tyco_fun naming "fun" = SOME "fun"
   1.295 +      | lookup_tyco_fun naming tyco = Code_Thingol.lookup_tyco naming tyco;
   1.296 +    val (names_class, class') = distill_names Code_Thingol.lookup_class class;
   1.297 +    val class'' = class'
   1.298 +      |> (Symtab.map o apsnd) (fn class_params => fn c' =>
   1.299 +          case lookup_classparam_rev c'
   1.300 +           of SOME c => class_params c
   1.301 +            | NONE => NONE)
   1.302 +    val names_inst = map_filter (Code_Thingol.lookup_instance naming)
   1.303 +      (StringPairTab.keys instance);
   1.304 +    val (names_tyco, tyco') = distill_names lookup_tyco_fun tyco;
   1.305 +    val (names_const, const') = distill_names Code_Thingol.lookup_const const;
   1.306 +    val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
   1.307 +    val names2 = subtract (op =) names_hidden names1;
   1.308 +    val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
   1.309 +    val names_all = Graph.all_succs program2 names2;
   1.310 +    val program4 = Graph.subgraph (member (op =) names_all) program3;
   1.311      val empty_funs = filter_out (member (op =) abortable)
   1.312        (Code_Thingol.empty_funs program3);
   1.313      val _ = if null empty_funs then () else error ("No defining equations for "
   1.314 -      ^ commas (map (Code_Name.labelled_name thy) empty_funs));
   1.315 +      ^ commas (map (Sign.extern_const thy) empty_funs));
   1.316    in
   1.317 -    serializer module args (Code_Name.labelled_name thy) reserved includes
   1.318 -      (Symtab.lookup module_alias) (Symtab.lookup class)
   1.319 -      (Symtab.lookup tyco) (Symtab.lookup const)
   1.320 -      program4 cs2
   1.321 +    serializer module args (labelled_name thy program2) reserved includes
   1.322 +      (Symtab.lookup module_alias) (Symtab.lookup class'')
   1.323 +      (Symtab.lookup tyco') (Symtab.lookup const')
   1.324 +      naming program4 names2
   1.325    end;
   1.326  
   1.327 -fun mount_serializer thy alt_serializer target =
   1.328 +fun mount_serializer thy alt_serializer target module args naming program =
   1.329    let
   1.330      val (targets, abortable) = CodeTargetData.get thy;
   1.331      fun collapse_hierarchy target =
   1.332 @@ -422,7 +451,7 @@
   1.333         of Serializer _ => (I, data)
   1.334          | Extends (super, modify) => let
   1.335              val (modify', data') = collapse_hierarchy super
   1.336 -          in (modify' #> modify, merge_target false target (data', data)) end
   1.337 +          in (modify' #> modify naming, merge_target false target (data', data)) end
   1.338        end;
   1.339      val (modify, data) = collapse_hierarchy target;
   1.340      val (serializer, _) = the_default (case the_serializer data
   1.341 @@ -430,18 +459,22 @@
   1.342      val reserved = the_reserved data;
   1.343      val includes = Symtab.dest (the_includes data);
   1.344      val module_alias = the_module_alias data;
   1.345 -    val { class, inst, tyco, const } = the_name_syntax data;
   1.346 +    val { class, instance, tyco, const } = the_name_syntax data;
   1.347    in
   1.348 -    invoke_serializer thy modify abortable serializer reserved
   1.349 -      includes module_alias class inst tyco const
   1.350 +    invoke_serializer thy abortable serializer reserved
   1.351 +      includes module_alias class instance tyco const module args naming (modify program)
   1.352    end;
   1.353  
   1.354 +in
   1.355 +
   1.356  fun serialize thy = mount_serializer thy NONE;
   1.357  
   1.358 -fun serialize_custom thy (target_name, seri) program cs =
   1.359 -  mount_serializer thy (SOME seri) target_name NONE [] program cs (String [])
   1.360 +fun serialize_custom thy (target_name, seri) naming program cs =
   1.361 +  mount_serializer thy (SOME seri) target_name NONE [] naming program cs (String [])
   1.362    |> the;
   1.363  
   1.364 +end; (* local *)
   1.365 +
   1.366  fun parse_args f args =
   1.367    case Scan.read OuterLex.stopper f args
   1.368     of SOME x => x
   1.369 @@ -450,40 +483,47 @@
   1.370  
   1.371  (* code presentation *)
   1.372  
   1.373 -fun code_of thy target module_name cs stmt_names =
   1.374 +fun code_of thy target module_name cs names_stmt =
   1.375    let
   1.376 -    val (cs', program) = Code_Thingol.consts_program thy cs;
   1.377 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
   1.378    in
   1.379 -    string stmt_names (serialize thy target (SOME module_name) [] program cs')
   1.380 +    string names_stmt (serialize thy target (SOME module_name) []
   1.381 +      naming program names_cs)
   1.382    end;
   1.383  
   1.384  
   1.385  (* code generation *)
   1.386  
   1.387 +fun transitivly_non_empty_funs thy naming program =
   1.388 +  let
   1.389 +    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
   1.390 +    val names = map_filter (Code_Thingol.lookup_const naming) cs;
   1.391 +  in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
   1.392 +
   1.393  fun read_const_exprs thy cs =
   1.394    let
   1.395      val (cs1, cs2) = Code_Name.read_const_exprs thy cs;
   1.396 -    val (cs3, program) = Code_Thingol.consts_program thy cs2;
   1.397 -    val cs4 = Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy);
   1.398 +    val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
   1.399 +    val names4 = transitivly_non_empty_funs thy naming program;
   1.400      val cs5 = map_filter
   1.401 -      (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
   1.402 +      (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
   1.403    in fold (insert (op =)) cs5 cs1 end;
   1.404  
   1.405  fun cached_program thy = 
   1.406    let
   1.407 -    val program = Code_Thingol.cached_program thy;
   1.408 -  in (Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
   1.409 +    val (naming, program) = Code_Thingol.cached_program thy;
   1.410 +  in (transitivly_non_empty_funs thy naming program, (naming, program)) end
   1.411  
   1.412  fun export_code thy cs seris =
   1.413    let
   1.414 -    val (cs', program) = if null cs then cached_program thy
   1.415 +    val (cs', (naming, program)) = if null cs then cached_program thy
   1.416        else Code_Thingol.consts_program thy cs;
   1.417      fun mk_seri_dest dest = case dest
   1.418       of NONE => compile
   1.419        | SOME "-" => export
   1.420        | SOME f => file (Path.explode f)
   1.421      val _ = map (fn (((target, module), dest), args) =>
   1.422 -      (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
   1.423 +      (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris;
   1.424    in () end;
   1.425  
   1.426  fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
   1.427 @@ -563,13 +603,6 @@
   1.428    OuterSyntax.command "export_code" "generate executable code for constants"
   1.429      K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   1.430  
   1.431 -fun shell_command thyname cmd = Toplevel.program (fn _ =>
   1.432 -  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd))
   1.433 -    ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
   1.434 -   of SOME f => (writeln "Now generating code..."; f (theory thyname))
   1.435 -    | NONE => error ("Bad directive " ^ quote cmd)))
   1.436 -  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
   1.437 -
   1.438  end; (*local*)
   1.439  
   1.440  end; (*struct*)