--- 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*)
--- 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
--- 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)
--- 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))
--- 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)
}
})
}
--- 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
}
}
--- 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) })
}
})
}
--- 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 *)
--- 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 */
--- 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
--- 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 =
--- 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 })
}
--- 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)
{
--- 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)
}
--- 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))
--- 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 *)
--- 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
}