# HG changeset patch
# User wenzelm
# Date 1681562578 -7200
# Node ID e6de70b781173d765baae75ccb9ee31d827e5f53
# Parent  ff801186ff66996ed1e87e19f2dc022b26bf025e
tuned signature;

diff -r ff801186ff66 -r e6de70b78117 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Sat Apr 15 14:14:30 2023 +0200
+++ b/src/Pure/General/long_name.ML	Sat Apr 15 14:42:58 2023 +0200
@@ -7,6 +7,8 @@
 signature LONG_NAME =
 sig
   val separator: string
+  val append: string -> string -> string
+  val qualify: string -> string -> string
   val is_qualified: string -> bool
   val qualifier: string -> string
   val base_name: string -> string
@@ -18,8 +20,6 @@
   val dest_local: string -> string option
   val implode: string list -> string
   val explode: string -> string list
-  val append: string -> string -> string
-  val qualify: string -> string -> string
   val map_base_name: (string -> string) -> string -> string
   type chunks
   val count_chunks: chunks -> int
@@ -42,6 +42,14 @@
 val separator = ".";
 val separator_char = String.nth separator 0;
 
+fun append name1 "" = name1
+  | append "" name2 = name2
+  | append name1 name2 = name1 ^ separator ^ name2;
+
+fun qualify qual name =
+  if qual = "" orelse name = "" then name
+  else qual ^ separator ^ name;
+
 fun last_separator name =
   let fun last i = if i < 0 orelse String.nth name i = separator_char then i else last (i - 1)
   in last (size name - 1) end;
@@ -72,14 +80,6 @@
 val implode = space_implode separator;
 val explode = space_explode separator;
 
-fun append name1 "" = name1
-  | append "" name2 = name2
-  | append name1 name2 = name1 ^ separator ^ name2;
-
-fun qualify qual name =
-  if qual = "" orelse name = "" then name
-  else qual ^ separator ^ name;
-
 fun map_base_name _ "" = ""
   | map_base_name f name =
       let val names = explode name