more exports: avoid clones in AFP;
authorwenzelm
Wed, 27 Mar 2019 23:55:39 +0100
changeset 70001 6430327079c2
parent 70000 93a95a24da82
child 70002 0addec5ab4ad
more exports: avoid clones in AFP;
src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Mar 27 22:15:36 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Mar 27 23:55:39 2019 +0100
@@ -22,6 +22,8 @@
 
   val export_code: bool -> string list
     -> (((string * string) * Path.T option option) * Token.T list) list -> theory -> theory
+  val export_code_cmd: bool -> string list
+    -> (((string * string) * (string * Position.T) option) * Token.T list) list -> theory -> theory
   val produce_code: Proof.context -> bool -> string list
     -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
   val present_code: Proof.context -> string list -> Code_Symbol.T list