src/Tools/Code/code_target.ML

     val names4 = transitivly_non_empty_funs thy naming program;
     val cs5 = map_filter
       (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
   in fold (insert (op =)) cs5 cs1 end;
 
-fun cached_program thy = 
-  let
-    val (naming, program) = Code_Thingol.cached_program thy;
-  in (transitivly_non_empty_funs thy naming program, (naming, program)) end
-
 fun export_code thy cs seris =
   let
-    val (cs', (naming, program)) = if null cs then cached_program thy
-      else Code_Thingol.consts_program thy cs;
+    val (cs', (naming, program)) = Code_Thingol.consts_program thy cs;
     fun mk_seri_dest dest = case dest
      of NONE => compile
       | SOME "-" => export
       | SOME f => file (Path.explode f)
     val _ = map (fn (((target, module), dest), args) =>

 (** Isar setup **)
 
 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
 
 val code_exprP =
-  (Scan.repeat P.term_group
+  (Scan.repeat1 P.term_group
   -- Scan.repeat (P.$$$ inK |-- P.name
      -- Scan.option (P.$$$ module_nameK |-- P.name)
      -- Scan.option (P.$$$ fileK |-- P.name)
      -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
   ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));