src/Pure/Admin/build_foiltex.scala
changeset 77566 2a99fcb283ee
parent 77565 fd87490429aa
child 77567 b975f5aaf6b8
equal deleted inserted replaced
77565:fd87490429aa 77566:2a99fcb283ee
     1 /*  Title:      Pure/Admin/build_foiltex.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Build Isabelle component for FoilTeX.
       
     5 
       
     6 See also https://ctan.org/pkg/foiltex
       
     7 */
       
     8 
       
     9 package isabelle
       
    10 
       
    11 
       
    12 object Build_Foiltex {
       
    13   /* build FoilTeX component */
       
    14 
       
    15   val default_url = "https://mirrors.ctan.org/macros/latex/contrib/foiltex.zip"
       
    16 
       
    17   def build_foiltex(
       
    18     download_url: String = default_url,
       
    19     target_dir: Path = Path.current,
       
    20     progress: Progress = new Progress
       
    21   ): Unit = {
       
    22     Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
       
    23       Isabelle_System.with_tmp_dir("download") { download_dir =>
       
    24 
       
    25         /* download */
       
    26 
       
    27         Isabelle_System.download_file(download_url, download_file, progress = progress)
       
    28         Isabelle_System.extract(download_file, download_dir)
       
    29 
       
    30         val foiltex_dir = File.get_dir(download_dir, title = download_url)
       
    31 
       
    32 
       
    33         /* component */
       
    34 
       
    35         val README = Path.explode("README")
       
    36         val version = {
       
    37           val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r
       
    38           split_lines(File.read(foiltex_dir + README))
       
    39             .collectFirst({ case Version(v) => v })
       
    40             .getOrElse(error("Failed to detect version in " + README))
       
    41         }
       
    42 
       
    43         val component = "foiltex-" + version
       
    44         val component_dir =
       
    45           Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
       
    46 
       
    47         Isabelle_System.extract(download_file, component_dir.path, strip = true)
       
    48 
       
    49         Isabelle_System.bash("pdflatex foiltex.ins", cwd = component_dir.path.file).check
       
    50         (component_dir.path + Path.basic("foiltex.log")).file.delete()
       
    51 
       
    52 
       
    53         /* settings */
       
    54 
       
    55         component_dir.write_settings("""
       
    56 ISABELLE_FOILTEX_HOME="$COMPONENT"
       
    57 """)
       
    58 
       
    59 
       
    60         /* README */
       
    61 
       
    62         Isabelle_System.move_file(component_dir.README,
       
    63           component_dir.path + Path.basic("README.flt"))
       
    64 
       
    65         File.write(component_dir.README,
       
    66           """This is FoilTeX from
       
    67 """ + download_url + """
       
    68 
       
    69 
       
    70     Makarius
       
    71     """ + Date.Format.date(Date.now()) + "\n")
       
    72       }
       
    73     }
       
    74   }
       
    75 
       
    76 
       
    77   /* Isabelle tool wrapper */
       
    78 
       
    79   val isabelle_tool =
       
    80     Isabelle_Tool("build_foiltex", "build component for FoilTeX",
       
    81       Scala_Project.here,
       
    82       { args =>
       
    83         var target_dir = Path.current
       
    84         var download_url = default_url
       
    85 
       
    86         val getopts = Getopts("""
       
    87 Usage: isabelle build_foiltex [OPTIONS]
       
    88 
       
    89   Options are:
       
    90     -D DIR       target directory (default ".")
       
    91     -U URL       download URL (default: """" + default_url + """")
       
    92 
       
    93   Build component for FoilTeX: slides in LaTeX.
       
    94 """,
       
    95           "D:" -> (arg => target_dir = Path.explode(arg)),
       
    96           "U:" -> (arg => download_url = arg))
       
    97 
       
    98         val more_args = getopts(args)
       
    99         if (more_args.nonEmpty) getopts.usage()
       
   100 
       
   101         val progress = new Console_Progress()
       
   102 
       
   103         build_foiltex(download_url = download_url, target_dir = target_dir, progress = progress)
       
   104       })
       
   105 }