# HG changeset patch
# User wenzelm
# Date 1553727339 -3600
# Node ID 6430327079c2c1c35a311c39d588130a0ed921ed
# Parent  93a95a24da82b3d7eb81f67ccc99f0a40908b53b
more exports: avoid clones in AFP;

diff -r 93a95a24da82 -r 6430327079c2 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