# HG changeset patch
# User wenzelm
# Date 1496346216 -7200
# Node ID ee4cf96a9406983d4be2961ef4aecc95f3681ac6
# Parent  d07300e8a14d7cb62a33e4c1e0f68b656e77f29c
tuned signature;

diff -r d07300e8a14d -r ee4cf96a9406 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Jun 01 21:43:36 2017 +0200
@@ -955,15 +955,13 @@
   let
     val config =
       {cautious = cautious,
-       problem_name =
-        SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
-         file_name))}
+       problem_name = SOME (TPTP_Problem_Name.parse_problem_name (Path.base_name file_name))}
   in interpret_file' config [] path_prefixes file_name end
 
 fun import_file cautious path_prefixes file_name type_map const_map thy =
   let
     val prob_name =
-      TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
+      TPTP_Problem_Name.parse_problem_name (Path.base_name file_name)
     val (result, thy') =
       interpret_file cautious path_prefixes file_name type_map const_map thy
   (*FIXME doesn't check if problem has already been interpreted*)
diff -r d07300e8a14d -r ee4cf96a9406 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Thu Jun 01 21:43:36 2017 +0200
@@ -1790,8 +1790,7 @@
  (on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
   let
     val prob_name =
-      Path.base file_name
-      |> Path.implode
+      Path.base_name file_name
       |> TPTP_Problem_Name.parse_problem_name
     val thy1 = TPTP_Interpret.import_file cautious path_prefixes file_name [] [] thy
     val fms = get_fmlas_of_prob thy1 prob_name
diff -r d07300e8a14d -r ee4cf96a9406 src/HOL/TPTP/TPTP_Parser_Test.thy
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Thu Jun 01 21:43:36 2017 +0200
@@ -47,8 +47,7 @@
 
 (*test against all TPTP problems*)
 fun problem_names () =
-    map (Path.base #>
-         Path.implode #>
+    map (Path.base_name #>
          TPTP_Problem_Name.parse_problem_name #>
          TPTP_Problem_Name.mangle_problem_name)
      (TPTP_Syntax.get_file_list tptp_probs_dir)
diff -r d07300e8a14d -r ee4cf96a9406 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Jun 01 21:43:36 2017 +0200
@@ -58,7 +58,7 @@
 
 val prob_names =
   probs
-  |> map (Path.base #> Path.implode #> TPTP_Problem_Name.Nonstandard)
+  |> map (Path.base_name #> TPTP_Problem_Name.Nonstandard)
 \<close>
 
 setup \<open>
@@ -575,7 +575,9 @@
 fun test_partial_reconstruction thy prob_file =
   let
     val prob_name =
-      (Path.base #> Path.implode #> TPTP_Problem_Name.Nonstandard) prob_file
+      prob_file
+      |> Path.base_name
+      |> TPTP_Problem_Name.Nonstandard
 
     val thy' =
       try
@@ -658,8 +660,7 @@
       val ctxt = Proof_Context.init_global thy' (*FIXME pass ctxt instead of thy*)
       val prob_name =
         file
-        |> Path.base
-        |> Path.implode
+        |> Path.base_name
         |> TPTP_Problem_Name.Nonstandard
     in
       Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -211,7 +211,7 @@
       val build_end = Date.now()
 
       val build_info: Build_Log.Build_Info =
-        Build_Log.Log_File(log_path.base.implode, build_result.out_lines).
+        Build_Log.Log_File(log_path.base_name, build_result.out_lines).
           parse_build_info(ml_statistics = true)
 
 
@@ -489,7 +489,7 @@
         val log = Path.explode(line)
         val bytes = ssh.read_bytes(log)
         ssh.rm(log)
-        (log.base.implode, bytes)
+        (log.base_name, bytes)
       }
     })
   }
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/General/graphics_file.scala
--- a/src/Pure/General/graphics_file.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/General/graphics_file.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -46,7 +46,7 @@
     val mapper = new DefaultFontMapper
     for {
       font <- Isabelle_System.fonts()
-      name <- Library.try_unsuffix(".ttf", font.base.implode)
+      name <- Library.try_unsuffix(".ttf", font.base_name)
     } {
       val parameters = new DefaultFontMapper.BaseFontParameters(File.platform_path(font))
       parameters.encoding = BaseFont.IDENTITY_H
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/General/http.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -137,7 +137,7 @@
 
   private lazy val html_fonts: SortedMap[String, Bytes] =
     SortedMap(
-      Isabelle_System.fonts(html = true).map(path => (path.base.implode -> Bytes.read(path))): _*)
+      Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
 
   def fonts(root: String = "/fonts"): Handler =
     get(root, uri =>
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/General/path.ML	Thu Jun 01 21:43:36 2017 +0200
@@ -29,6 +29,7 @@
   val print: T -> string
   val dir: T -> T
   val base: T -> T
+  val base_name: T -> string
   val ext: string -> T -> T
   val split_ext: T -> T * string
   val expand: T -> T
@@ -183,6 +184,7 @@
 
 val dir = split_path #1;
 val base = split_path (fn (_, s) => Path [Basic s]);
+val base_name = implode_path o base;
 
 fun ext "" = I
   | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/General/path.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -149,6 +149,7 @@
 
   def dir: Path = split_path._1
   def base: Path = new Path(List(Path.Basic(split_path._2)))
+  def base_name: String = base.implode
 
   def ext(e: String): Path =
     if (e == "") this
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/Thy/html.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -234,7 +234,7 @@
   }
 
   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
-    css: String = isabelle_css.base.implode, hidden: Boolean = true)
+    css: String = isabelle_css.base_name, hidden: Boolean = true)
   {
     init_dir(dir)
     File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden))
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -574,7 +574,7 @@
           val global_theories =
             for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
             yield {
-              val thy_name = Path.explode(thy).expand.base.implode
+              val thy_name = Path.explode(thy).expand.base_name
               if (Long_Name.is_qualified(thy_name))
                 error("Bad qualified name for global theory " +
                   quote(thy_name) + Position.here(pos))
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/Thy/thy_header.ML	Thu Jun 01 21:43:36 2017 +0200
@@ -114,7 +114,7 @@
 val ml_roots = ["ML_Root0", "ML_Root"];
 val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
 
-val import_name = Path.implode o Path.base o Path.explode;
+val import_name = Path.base_name o Path.explode;
 
 
 (* header args *)
diff -r d07300e8a14d -r ee4cf96a9406 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/Tools/spell_checker.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -57,7 +57,7 @@
 
   class Dictionary private[Spell_Checker](val path: Path)
   {
-    val lang = path.split_ext._1.base.implode
+    val lang = path.split_ext._1.base_name
     val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
     override def toString: String = lang
   }
diff -r d07300e8a14d -r ee4cf96a9406 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -193,7 +193,7 @@
           val path = Path.explode(text)
           val (dir, base_name) =
             if (text == "" || text.endsWith("/")) (path, "")
-            else (path.dir, path.base.implode)
+            else (path.dir, path.base_name)
 
           val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
           val files = directory.listFiles