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