# HG changeset patch
# User wenzelm
# Date 1543418071 -3600
# Node ID b6dacf6eabe3ba4ea84d5848a4f672dcbd5e789f
# Parent  c5b3860d29efb42df94f6f7fb8900ab801ae0bed
clarified signature;

diff -r c5b3860d29ef -r b6dacf6eabe3 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Nov 28 16:14:31 2018 +0100
@@ -955,13 +955,13 @@
   let
     val config =
       {cautious = cautious,
-       problem_name = SOME (TPTP_Problem_Name.parse_problem_name (Path.base_name file_name))}
+       problem_name = SOME (TPTP_Problem_Name.parse_problem_name (Path.file_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.base_name file_name)
+      TPTP_Problem_Name.parse_problem_name (Path.file_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 c5b3860d29ef -r b6dacf6eabe3 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Nov 28 16:14:31 2018 +0100
@@ -1790,7 +1790,7 @@
  (on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
   let
     val prob_name =
-      Path.base_name file_name
+      Path.file_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 c5b3860d29ef -r b6dacf6eabe3 src/HOL/TPTP/TPTP_Parser_Test.thy
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Nov 28 16:14:31 2018 +0100
@@ -47,7 +47,7 @@
 
 (*test against all TPTP problems*)
 fun problem_names () =
-    map (Path.base_name #>
+    map (Path.file_name #>
          TPTP_Problem_Name.parse_problem_name #>
          TPTP_Problem_Name.mangle_problem_name)
      (TPTP_Syntax.get_file_list tptp_probs_dir)
diff -r c5b3860d29ef -r b6dacf6eabe3 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Wed Nov 28 16:14:31 2018 +0100
@@ -58,7 +58,7 @@
 
 val prob_names =
   probs
-  |> map (Path.base_name #> TPTP_Problem_Name.Nonstandard)
+  |> map (Path.file_name #> TPTP_Problem_Name.Nonstandard)
 \<close>
 
 setup \<open>
@@ -576,7 +576,7 @@
   let
     val prob_name =
       prob_file
-      |> Path.base_name
+      |> Path.file_name
       |> TPTP_Problem_Name.Nonstandard
 
     val thy' =
@@ -660,7 +660,7 @@
       val ctxt = Proof_Context.init_global thy' (*FIXME pass ctxt instead of thy*)
       val prob_name =
         file
-        |> Path.base_name
+        |> Path.file_name
         |> TPTP_Problem_Name.Nonstandard
     in
       Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/Admin/build_history.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -246,7 +246,7 @@
       val build_end = Date.now()
 
       val build_info: Build_Log.Build_Info =
-        Build_Log.Log_File(log_path.base_name, build_result.out_lines).
+        Build_Log.Log_File(log_path.file_name, build_result.out_lines).
           parse_build_info(ml_statistics = true)
 
 
@@ -587,7 +587,7 @@
         val log = Path.explode(line)
         val bytes = ssh.read_bytes(log)
         ssh.rm(log)
-        (log.base_name, bytes)
+        (log.file_name, bytes)
       }
     })
   }
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -183,7 +183,7 @@
       for (file <- ldd_files) {
         bash(target,
           """install_name_tool -change """ + Bash.string(file) + " " +
-            Bash.string("@executable_path/" + Path.explode(file).base_name) + " poly").check
+            Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check
       }
     }
 
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/General/http.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -161,11 +161,11 @@
       {
         val uri_name = arg.uri.toString
         if (uri_name == root) {
-          Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.base_name))))
+          Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
         }
         else {
           html_fonts.collectFirst(
-            { case entry if uri_name == root + "/" + entry.path.base_name => Response(entry.bytes) })
+            { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) })
         }
       })
 }
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/General/path.ML	Wed Nov 28 16:14:31 2018 +0100
@@ -29,10 +29,10 @@
   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
+  val file_name: T -> string
   val smart_implode: T -> string
   val position: T -> Position.T
 end;
@@ -184,7 +184,6 @@
 
 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)));
@@ -207,6 +206,8 @@
 
 val expand = rep #> maps eval #> norm #> Path;
 
+val file_name = implode_path o base o expand;
+
 
 (* smart implode *)
 
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/General/path.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -149,7 +149,6 @@
 
   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
@@ -201,6 +200,8 @@
 
   def expand: Path = expand_env(Isabelle_System.settings())
 
+  def file_name: String = expand.base.implode
+
 
   /* source position */
 
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -306,7 +306,7 @@
         val path = Path.explode(text)
         val (dir, base_name) =
           if (text == "" || text.endsWith("/")) (path, "")
-          else (path.dir, path.base_name)
+          else (path.dir, path.file_name)
 
         val directory = new JFile(session.resources.append(snapshot.node_name, dir))
         val files = directory.listFiles
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/System/options.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -124,7 +124,7 @@
     }
 
     def parse_prefs(options: Options, content: String): Options =
-      parse_file(options, PREFS.base_name, content, syntax = prefs_syntax, parser = prefs_entry)
+      parse_file(options, PREFS.file_name, content, syntax = prefs_syntax, parser = prefs_entry)
   }
 
   def read_prefs(file: Path = PREFS): String =
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/Thy/bibtex.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -33,7 +33,7 @@
     {
       val name = snapshot.node_name
       if (detect(name.node)) {
-        val title = "Bibliography " + quote(snapshot.node_name.path.base_name)
+        val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
         val content =
           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
             File.write(bib, snapshot.node.source)
@@ -637,7 +637,7 @@
       val bib_files = bib.map(path => path.split_ext._1)
       val bib_names =
       {
-        val names0 = bib_files.map(_.base_name)
+        val names0 = bib_files.map(_.file_name)
         if (Library.duplicates(names0).isEmpty) names0
         else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
       }
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/Thy/html.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -363,7 +363,7 @@
         List(
           "@font-face {",
           "  font-family: '" + entry.family + "';",
-          "  src: url('" + make_url(entry.path.base_name) + "') format('truetype');") :::
+          "  src: url('" + make_url(entry.path.file_name) + "') format('truetype');") :::
         (if (entry.is_bold) List("  font-weight: bold;") else Nil) :::
         (if (entry.is_italic) List("  font-style: italic;") else Nil) :::
         List("}"))
@@ -390,7 +390,7 @@
   }
 
   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
-    css: String = isabelle_css.base_name,
+    css: String = isabelle_css.file_name,
     hidden: Boolean = true,
     structural: Boolean = true)
   {
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/Thy/present.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -124,7 +124,7 @@
     val name = snapshot.node_name
 
     if (plain_text) {
-      val title = "File " + quote(name.path.base_name)
+      val title = "File " + quote(name.path.file_name)
       val content = output_document(title, HTML.text(snapshot.node.source))
       Preview(title, content)
     }
@@ -134,7 +134,7 @@
         case None =>
           val title =
             if (name.is_theory) "Theory " + quote(name.theory_base_name)
-            else "File " + quote(name.path.base_name)
+            else "File " + quote(name.path.file_name)
           val content = output_document(title, pide_document(snapshot))
           Preview(title, content)
       }
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -532,7 +532,7 @@
     def bibtex_entries: List[Text.Info[String]] =
       (for {
         (document_dir, file) <- document_files.iterator
-        if Bibtex.is_bibtex(file.base_name)
+        if Bibtex.is_bibtex(file.file_name)
         info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
       } yield info).toList
   }
@@ -560,7 +560,7 @@
       val global_theories =
         for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
         yield {
-          val thy_name = Path.explode(thy).expand.base_name
+          val thy_name = Path.explode(thy).file_name
           if (Long_Name.is_qualified(thy_name))
             error("Bad qualified name for global theory " +
               quote(thy_name) + Position.here(pos))
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Nov 28 16:14:31 2018 +0100
@@ -121,7 +121,7 @@
 fun import_name s =
   if String.isSuffix ".thy" s then
     error ("Malformed theory import: " ^ quote s)
-  else Path.base_name (Path.explode s);
+  else Path.file_name (Path.explode s);
 
 
 (* header args *)
diff -r c5b3860d29ef -r b6dacf6eabe3 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Wed Nov 28 15:38:18 2018 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Wed Nov 28 16:14:31 2018 +0100
@@ -66,7 +66,7 @@
 
   class Dictionary private[Spell_Checker](val path: Path)
   {
-    val lang = path.split_ext._1.base_name
+    val lang = path.split_ext._1.file_name
     val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
     override def toString: String = lang
   }