# HG changeset patch
# User wenzelm
# Date 1655888971 -7200
# Node ID b2b097624e4c5115d753efd41f57689cdd836f14
# Parent  29654a8e937472007015f24223e693db47429ddc
clarified types and defaults;

diff -r 29654a8e9374 -r b2b097624e4c src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Tue Jun 21 23:36:16 2022 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jun 22 11:09:31 2022 +0200
@@ -47,13 +47,13 @@
     new Bytes(a, 0, a.length)
   }
 
-  object Decode_Base64 extends Scala.Fun("decode_base64") {
+  object Decode_Base64 extends Scala.Fun("decode_base64") with Scala.Fun_Single_Bytes {
     val here = Scala_Project.here
     def invoke(args: List[Bytes]): List[Bytes] =
       List(base64(Library.the_single(args).text))
   }
 
-  object Encode_Base64 extends Scala.Fun("encode_base64") {
+  object Encode_Base64 extends Scala.Fun("encode_base64") with Scala.Fun_Single_Bytes {
     val here = Scala_Project.here
     def invoke(args: List[Bytes]): List[Bytes] =
       List(Bytes(Library.the_single(args).base64))
@@ -62,13 +62,13 @@
 
   /* XZ compression */
 
-  object Compress extends Scala.Fun("compress") {
+  object Compress extends Scala.Fun("compress") with Scala.Fun_Single_Bytes {
     val here = Scala_Project.here
     def invoke(args: List[Bytes]): List[Bytes] =
       List(Library.the_single(args).compress())
   }
 
-  object Uncompress extends Scala.Fun("uncompress") {
+  object Uncompress extends Scala.Fun("uncompress") with Scala.Fun_Single_Bytes {
     val here = Scala_Project.here
     def invoke(args: List[Bytes]): List[Bytes] =
       List(Library.the_single(args).uncompress())
diff -r 29654a8e9374 -r b2b097624e4c src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Jun 21 23:36:16 2022 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed Jun 22 11:09:31 2022 +0200
@@ -13,7 +13,7 @@
      bibtex_entries: (string * string list) list,
      command_timings: Properties.T list,
      load_commands: (string * Position.T) list,
-     scala_functions: (string * (bool * Position.T)) list,
+     scala_functions: (string * ((bool * bool) * Position.T)) list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
   val init_session_yxml: string -> unit
@@ -25,7 +25,7 @@
   val last_timing: Toplevel.transition -> Time.time
   val check_load_command: Proof.context -> string * Position.T -> string
   val scala_functions: unit -> string list
-  val check_scala_function: Proof.context -> string * Position.T -> string * bool
+  val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool)
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -104,7 +104,7 @@
     bibtex_entries = Symtab.empty: string list Symtab.table,
     timings = empty_timings,
     load_commands = []: (string * Position.T) list,
-    scala_functions = Symtab.empty: (bool * Position.T) Symtab.table},
+    scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table},
    {global_theories = Symtab.empty: string Symtab.table,
     loaded_theories = Symtab.empty: unit Symtab.table});
 
@@ -137,7 +137,7 @@
             (pair (list (pair string string))
               (pair (list (pair string (list string))) (pair (list properties)
                 (pair (list (pair string properties))
-                  (pair (list (pair string (pair bool properties)))
+                  (pair (list (pair string (pair (pair bool bool) properties)))
                     (pair (list (pair string string)) (list string))))))))
         end;
   in
@@ -183,19 +183,18 @@
 (*raw bootstrap environment*)
 fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
 
+val scala_function_default = the_default ((true, false), Position.none);
+
 (*regular resources*)
 fun scala_function a =
-  (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a));
+  (a, scala_function_default (Symtab.lookup (get_session_base1 #scala_functions) a));
 
 fun check_scala_function ctxt arg =
   let
     val funs = scala_functions () |> sort_strings |> map scala_function;
     val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg;
-    val multi =
-      (case AList.lookup (op =) funs name of
-        SOME (multi, _) => multi
-      | NONE => false);
-  in (name, multi) end;
+    val flags = #1 (scala_function_default (AList.lookup (op =) funs name));
+  in (name, flags) end;
 
 val _ = Theory.setup
  (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
@@ -206,8 +205,10 @@
   ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
     (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) =>
       let
-        val (name, multi) = check_scala_function ctxt arg;
-        val func = if multi then "Scala.function" else "Scala.function1";
+        val (name, (single, bytes)) = check_scala_function ctxt arg;
+        val func =
+          (if single then "Scala.function1" else "Scala.function") ^
+          (if bytes then "_bytes" else "");
       in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end)));
 
 
diff -r 29654a8e9374 -r b2b097624e4c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Jun 21 23:36:16 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Jun 22 11:09:31 2022 +0200
@@ -46,14 +46,14 @@
       pair(list(pair(string, list(string))),
       pair(list(properties),
       pair(list(pair(string, properties)),
-      pair(list(pair(string, pair(bool, properties))),
+      pair(list(Scala.encode_fun),
       pair(list(pair(string, string)), list(string))))))))(
        (sessions_structure.session_positions,
        (sessions_structure.dest_session_directories,
        (sessions_structure.bibtex_entries,
        (command_timings,
        (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
-       (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))),
+       (Scala.functions,
        (session_base.global_theories.toList,
         session_base.loaded_theories.keys)))))))))
   }
diff -r 29654a8e9374 -r b2b097624e4c src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Tue Jun 21 23:36:16 2022 +0200
+++ b/src/Pure/System/scala.scala	Wed Jun 22 11:09:31 2022 +0200
@@ -18,12 +18,17 @@
 
   abstract class Fun(val name: String, val thread: Boolean = false) {
     override def toString: String = name
-    def multi: Boolean = true
+    def single: Boolean = false
+    def bytes: Boolean = false
     def position: Properties.T = here.position
     def here: Scala_Project.Here
     def invoke(args: List[Bytes]): List[Bytes]
   }
 
+  trait Fun_Single extends Fun { override def single: Boolean = true }
+  trait Fun_Bytes extends Fun { override def bytes: Boolean = true }
+  trait Fun_Single_Bytes extends Fun_Single with Fun_Bytes
+
   abstract class Fun_Strings(name: String, thread: Boolean = false)
   extends Fun(name, thread = thread) {
     override def invoke(args: List[Bytes]): List[Bytes] =
@@ -32,13 +37,18 @@
   }
 
   abstract class Fun_String(name: String, thread: Boolean = false)
-  extends Fun_Strings(name, thread = thread) {
-    override def multi: Boolean = false
+  extends Fun_Strings(name, thread = thread) with Fun_Single {
     override def apply(args: List[String]): List[String] =
       List(apply(Library.the_single(args)))
     def apply(arg: String): String
   }
 
+  val encode_fun: XML.Encode.T[Fun] = { fun =>
+    import XML.Encode._
+    pair(string, pair(pair(bool, bool), properties))(
+      fun.name, ((fun.single, fun.bytes), fun.position))
+  }
+
   class Functions(val functions: Fun*) extends Isabelle_System.Service
 
   lazy val functions: List[Fun] =