tuned signature;
authorwenzelm
Thu Jun 01 21:43:36 2017 +0200 (2017-06-01)
changeset 65999ee4cf96a9406
parent 65998 d07300e8a14d
child 66000 58aa6749ff36
tuned signature;
src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
src/HOL/TPTP/TPTP_Parser_Test.thy
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
src/Pure/Admin/build_history.scala
src/Pure/General/graphics_file.scala
src/Pure/General/http.scala
src/Pure/General/path.ML
src/Pure/General/path.scala
src/Pure/Thy/html.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.ML
src/Pure/Tools/spell_checker.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Jun 01 21:24:33 2017 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Jun 01 21:43:36 2017 +0200
     1.3 @@ -955,15 +955,13 @@
     1.4    let
     1.5      val config =
     1.6        {cautious = cautious,
     1.7 -       problem_name =
     1.8 -        SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
     1.9 -         file_name))}
    1.10 +       problem_name = SOME (TPTP_Problem_Name.parse_problem_name (Path.base_name file_name))}
    1.11    in interpret_file' config [] path_prefixes file_name end
    1.12  
    1.13  fun import_file cautious path_prefixes file_name type_map const_map thy =
    1.14    let
    1.15      val prob_name =
    1.16 -      TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
    1.17 +      TPTP_Problem_Name.parse_problem_name (Path.base_name file_name)
    1.18      val (result, thy') =
    1.19        interpret_file cautious path_prefixes file_name type_map const_map thy
    1.20    (*FIXME doesn't check if problem has already been interpreted*)
     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Thu Jun 01 21:24:33 2017 +0200
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Thu Jun 01 21:43:36 2017 +0200
     2.3 @@ -1790,8 +1790,7 @@
     2.4   (on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
     2.5    let
     2.6      val prob_name =
     2.7 -      Path.base file_name
     2.8 -      |> Path.implode
     2.9 +      Path.base_name file_name
    2.10        |> TPTP_Problem_Name.parse_problem_name
    2.11      val thy1 = TPTP_Interpret.import_file cautious path_prefixes file_name [] [] thy
    2.12      val fms = get_fmlas_of_prob thy1 prob_name
     3.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Thu Jun 01 21:24:33 2017 +0200
     3.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Thu Jun 01 21:43:36 2017 +0200
     3.3 @@ -47,8 +47,7 @@
     3.4  
     3.5  (*test against all TPTP problems*)
     3.6  fun problem_names () =
     3.7 -    map (Path.base #>
     3.8 -         Path.implode #>
     3.9 +    map (Path.base_name #>
    3.10           TPTP_Problem_Name.parse_problem_name #>
    3.11           TPTP_Problem_Name.mangle_problem_name)
    3.12       (TPTP_Syntax.get_file_list tptp_probs_dir)
     4.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Jun 01 21:24:33 2017 +0200
     4.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Jun 01 21:43:36 2017 +0200
     4.3 @@ -58,7 +58,7 @@
     4.4  
     4.5  val prob_names =
     4.6    probs
     4.7 -  |> map (Path.base #> Path.implode #> TPTP_Problem_Name.Nonstandard)
     4.8 +  |> map (Path.base_name #> TPTP_Problem_Name.Nonstandard)
     4.9  \<close>
    4.10  
    4.11  setup \<open>
    4.12 @@ -575,7 +575,9 @@
    4.13  fun test_partial_reconstruction thy prob_file =
    4.14    let
    4.15      val prob_name =
    4.16 -      (Path.base #> Path.implode #> TPTP_Problem_Name.Nonstandard) prob_file
    4.17 +      prob_file
    4.18 +      |> Path.base_name
    4.19 +      |> TPTP_Problem_Name.Nonstandard
    4.20  
    4.21      val thy' =
    4.22        try
    4.23 @@ -658,8 +660,7 @@
    4.24        val ctxt = Proof_Context.init_global thy' (*FIXME pass ctxt instead of thy*)
    4.25        val prob_name =
    4.26          file
    4.27 -        |> Path.base
    4.28 -        |> Path.implode
    4.29 +        |> Path.base_name
    4.30          |> TPTP_Problem_Name.Nonstandard
    4.31      in
    4.32        Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
     5.1 --- a/src/Pure/Admin/build_history.scala	Thu Jun 01 21:24:33 2017 +0200
     5.2 +++ b/src/Pure/Admin/build_history.scala	Thu Jun 01 21:43:36 2017 +0200
     5.3 @@ -211,7 +211,7 @@
     5.4        val build_end = Date.now()
     5.5  
     5.6        val build_info: Build_Log.Build_Info =
     5.7 -        Build_Log.Log_File(log_path.base.implode, build_result.out_lines).
     5.8 +        Build_Log.Log_File(log_path.base_name, build_result.out_lines).
     5.9            parse_build_info(ml_statistics = true)
    5.10  
    5.11  
    5.12 @@ -489,7 +489,7 @@
    5.13          val log = Path.explode(line)
    5.14          val bytes = ssh.read_bytes(log)
    5.15          ssh.rm(log)
    5.16 -        (log.base.implode, bytes)
    5.17 +        (log.base_name, bytes)
    5.18        }
    5.19      })
    5.20    }
     6.1 --- a/src/Pure/General/graphics_file.scala	Thu Jun 01 21:24:33 2017 +0200
     6.2 +++ b/src/Pure/General/graphics_file.scala	Thu Jun 01 21:43:36 2017 +0200
     6.3 @@ -46,7 +46,7 @@
     6.4      val mapper = new DefaultFontMapper
     6.5      for {
     6.6        font <- Isabelle_System.fonts()
     6.7 -      name <- Library.try_unsuffix(".ttf", font.base.implode)
     6.8 +      name <- Library.try_unsuffix(".ttf", font.base_name)
     6.9      } {
    6.10        val parameters = new DefaultFontMapper.BaseFontParameters(File.platform_path(font))
    6.11        parameters.encoding = BaseFont.IDENTITY_H
     7.1 --- a/src/Pure/General/http.scala	Thu Jun 01 21:24:33 2017 +0200
     7.2 +++ b/src/Pure/General/http.scala	Thu Jun 01 21:43:36 2017 +0200
     7.3 @@ -137,7 +137,7 @@
     7.4  
     7.5    private lazy val html_fonts: SortedMap[String, Bytes] =
     7.6      SortedMap(
     7.7 -      Isabelle_System.fonts(html = true).map(path => (path.base.implode -> Bytes.read(path))): _*)
     7.8 +      Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
     7.9  
    7.10    def fonts(root: String = "/fonts"): Handler =
    7.11      get(root, uri =>
     8.1 --- a/src/Pure/General/path.ML	Thu Jun 01 21:24:33 2017 +0200
     8.2 +++ b/src/Pure/General/path.ML	Thu Jun 01 21:43:36 2017 +0200
     8.3 @@ -29,6 +29,7 @@
     8.4    val print: T -> string
     8.5    val dir: T -> T
     8.6    val base: T -> T
     8.7 +  val base_name: T -> string
     8.8    val ext: string -> T -> T
     8.9    val split_ext: T -> T * string
    8.10    val expand: T -> T
    8.11 @@ -183,6 +184,7 @@
    8.12  
    8.13  val dir = split_path #1;
    8.14  val base = split_path (fn (_, s) => Path [Basic s]);
    8.15 +val base_name = implode_path o base;
    8.16  
    8.17  fun ext "" = I
    8.18    | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
     9.1 --- a/src/Pure/General/path.scala	Thu Jun 01 21:24:33 2017 +0200
     9.2 +++ b/src/Pure/General/path.scala	Thu Jun 01 21:43:36 2017 +0200
     9.3 @@ -149,6 +149,7 @@
     9.4  
     9.5    def dir: Path = split_path._1
     9.6    def base: Path = new Path(List(Path.Basic(split_path._2)))
     9.7 +  def base_name: String = base.implode
     9.8  
     9.9    def ext(e: String): Path =
    9.10      if (e == "") this
    10.1 --- a/src/Pure/Thy/html.scala	Thu Jun 01 21:24:33 2017 +0200
    10.2 +++ b/src/Pure/Thy/html.scala	Thu Jun 01 21:43:36 2017 +0200
    10.3 @@ -234,7 +234,7 @@
    10.4    }
    10.5  
    10.6    def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
    10.7 -    css: String = isabelle_css.base.implode, hidden: Boolean = true)
    10.8 +    css: String = isabelle_css.base_name, hidden: Boolean = true)
    10.9    {
   10.10      init_dir(dir)
   10.11      File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden))
    11.1 --- a/src/Pure/Thy/sessions.scala	Thu Jun 01 21:24:33 2017 +0200
    11.2 +++ b/src/Pure/Thy/sessions.scala	Thu Jun 01 21:43:36 2017 +0200
    11.3 @@ -574,7 +574,7 @@
    11.4            val global_theories =
    11.5              for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
    11.6              yield {
    11.7 -              val thy_name = Path.explode(thy).expand.base.implode
    11.8 +              val thy_name = Path.explode(thy).expand.base_name
    11.9                if (Long_Name.is_qualified(thy_name))
   11.10                  error("Bad qualified name for global theory " +
   11.11                    quote(thy_name) + Position.here(pos))
    12.1 --- a/src/Pure/Thy/thy_header.ML	Thu Jun 01 21:24:33 2017 +0200
    12.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Jun 01 21:43:36 2017 +0200
    12.3 @@ -114,7 +114,7 @@
    12.4  val ml_roots = ["ML_Root0", "ML_Root"];
    12.5  val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
    12.6  
    12.7 -val import_name = Path.implode o Path.base o Path.explode;
    12.8 +val import_name = Path.base_name o Path.explode;
    12.9  
   12.10  
   12.11  (* header args *)
    13.1 --- a/src/Pure/Tools/spell_checker.scala	Thu Jun 01 21:24:33 2017 +0200
    13.2 +++ b/src/Pure/Tools/spell_checker.scala	Thu Jun 01 21:43:36 2017 +0200
    13.3 @@ -57,7 +57,7 @@
    13.4  
    13.5    class Dictionary private[Spell_Checker](val path: Path)
    13.6    {
    13.7 -    val lang = path.split_ext._1.base.implode
    13.8 +    val lang = path.split_ext._1.base_name
    13.9      val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
   13.10      override def toString: String = lang
   13.11    }
    14.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Jun 01 21:24:33 2017 +0200
    14.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Jun 01 21:43:36 2017 +0200
    14.3 @@ -193,7 +193,7 @@
    14.4            val path = Path.explode(text)
    14.5            val (dir, base_name) =
    14.6              if (text == "" || text.endsWith("/")) (path, "")
    14.7 -            else (path.dir, path.base.implode)
    14.8 +            else (path.dir, path.base_name)
    14.9  
   14.10            val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
   14.11            val files = directory.listFiles