# HG changeset patch
# User wenzelm
# Date 1565434415 -7200
# Node ID f389019024ceee21cc89c6f64ec8c402d0c13acd
# Parent  de75eea6ffc88bccfc57749a5fbcc9b393438f3d
allow duplicate exports via strict = false;

diff -r de75eea6ffc8 -r f389019024ce src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Aug 10 10:31:56 2019 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Aug 10 12:53:35 2019 +0200
@@ -232,7 +232,8 @@
     theory_name: string,
     name: string,
     executable: bool,
-    compress: bool}
+    compress: bool,
+    strict: bool}
   val export: export_args -> Properties.T
   val debugger_state: string -> Properties.T
   val debugger_output: string -> Properties.T
@@ -718,16 +719,18 @@
   theory_name: string,
   name: string,
   executable: bool,
-  compress: bool};
+  compress: bool,
+  strict: bool};
 
-fun export ({id, serial, theory_name, name, executable, compress}: export_args) =
+fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) =
  [(functionN, exportN),
   (idN, the_default "" id),
   (serialN, Value.print_int serial),
   ("theory_name", theory_name),
   (nameN, name),
   ("executable", Value.print_bool executable),
-  ("compress", Value.print_bool compress)];
+  ("compress", Value.print_bool compress),
+  ("strict", Value.print_bool strict)];
 
 
 (* debugger *)
diff -r de75eea6ffc8 -r f389019024ce src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Aug 10 10:31:56 2019 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Aug 10 12:53:35 2019 +0200
@@ -632,11 +632,13 @@
       theory_name: String,
       name: String,
       executable: Boolean,
-      compress: Boolean)
+      compress: Boolean,
+      strict: Boolean)
 
     val THEORY_NAME = "theory_name"
     val EXECUTABLE = "executable"
     val COMPRESS = "compress"
+    val STRICT = "strict"
 
     def dest_inline(props: Properties.T): Option[(Args, Path)] =
       props match {
@@ -647,8 +649,9 @@
             (NAME, name),
             (EXECUTABLE, Value.Boolean(executable)),
             (COMPRESS, Value.Boolean(compress)),
+            (STRICT, Value.Boolean(strict)),
             (FILE, file)) if isabelle.Path.is_valid(file) =>
-          val args = Args(None, serial, theory_name, name, executable, compress)
+          val args = Args(None, serial, theory_name, name, executable, compress, strict)
           Some((args, isabelle.Path.explode(file)))
         case _ => None
       }
@@ -662,8 +665,9 @@
             (THEORY_NAME, theory_name),
             (NAME, name),
             (EXECUTABLE, Value.Boolean(executable)),
-            (COMPRESS, Value.Boolean(compress))) =>
-          Some(Args(proper_string(id), serial, theory_name, name, executable, compress))
+            (COMPRESS, Value.Boolean(compress)),
+            (STRICT, Value.Boolean(strict))) =>
+          Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict))
         case _ => None
       }
   }
diff -r de75eea6ffc8 -r f389019024ce src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Sat Aug 10 10:31:56 2019 +0200
+++ b/src/Pure/Thy/export.ML	Sat Aug 10 12:53:35 2019 +0200
@@ -7,7 +7,8 @@
 signature EXPORT =
 sig
   val report_export: theory -> Path.binding -> unit
-  type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}
+  type params =
+    {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
   val export_params: params -> string list -> unit
   val export: theory -> Path.binding -> string list -> unit
   val export_executable: theory -> Path.binding -> string list -> unit
@@ -29,9 +30,10 @@
     val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path));
   in Context_Position.report_generic (Context.Theory thy) pos markup end;
 
-type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool};
+type params =
+  {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
 
-fun export_params ({theory = thy, binding, executable, compress}: params) blob =
+fun export_params ({theory = thy, binding, executable, compress, strict}: params) blob =
  (report_export thy binding;
   (Output.try_protocol_message o Markup.export)
    {id = Position.get_id (Position.thread_data ()),
@@ -39,13 +41,16 @@
     theory_name = Context.theory_long_name thy,
     name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
-    compress = compress} blob);
+    compress = compress,
+    strict = strict} blob);
 
 fun export thy binding blob =
-  export_params {theory = thy, binding = binding, executable = false, compress = true} blob;
+  export_params
+    {theory = thy, binding = binding, executable = false, compress = true, strict = true} blob;
 
 fun export_executable thy binding blob =
-  export_params {theory = thy, binding = binding, executable = true, compress = true} blob;
+  export_params
+    {theory = thy, binding = binding, executable = true, compress = true, strict = true} blob;
 
 fun export_file thy binding file = export thy binding [File.read file];
 fun export_executable_file thy binding file = export_executable thy binding [File.read file];
diff -r de75eea6ffc8 -r f389019024ce src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 10 10:31:56 2019 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 10 12:53:35 2019 +0200
@@ -189,13 +189,16 @@
     private val errors = Synchronized[List[String]](Nil)
 
     private val consumer =
-      Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
+      Consumer_Thread.fork(name = "export")(consume = (arg: (Entry, Boolean)) =>
         {
+          val (entry, strict) = arg
           entry.body.join
           db.transaction {
             if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
-              val msg = message("Duplicate export", entry.theory_name, entry.name)
-              errors.change(msg :: _)
+              if (strict) {
+                val msg = message("Duplicate export", entry.theory_name, entry.name)
+                errors.change(msg :: _)
+              }
             }
             else entry.write(db)
           }
@@ -203,7 +206,7 @@
         })
 
     def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
-      consumer.send(make_entry(session_name, args, body, cache = cache))
+      consumer.send(make_entry(session_name, args, body, cache = cache) -> args.strict)
 
     def shutdown(close: Boolean = false): List[String] =
     {