src/Pure/Tools/logo.scala
author wenzelm
Fri, 01 Apr 2022 23:19:12 +0200
changeset 75394 42267c650205
parent 75393 87ebf5a50283
child 76883 186e07be32c3
permissions -rw-r--r--
tuned formatting;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/logo.scala
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     3
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     4
Create variants of the Isabelle logo (PDF).
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     5
*/
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     6
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     7
package isabelle
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     8
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
     9
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73723
diff changeset
    10
object Logo {
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    11
  /* create logo */
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    12
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73723
diff changeset
    13
  def make_output_file(logo_name: String): Path = {
73723
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    14
    val name = if (logo_name.isEmpty) "isabelle" else "isabelle_" + Word.lowercase(logo_name)
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    15
    Path.explode(name).pdf
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    16
  }
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    17
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73723
diff changeset
    18
  def create_logo(logo_name: String, output_file: Path, quiet: Boolean = false): Unit = {
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    19
    Isabelle_System.with_tmp_file("logo", ext = "eps") { tmp_file =>
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    20
      val template = File.read(Path.explode("$ISABELLE_HOME/lib/logo/isabelle_any.eps"))
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    21
      File.write(tmp_file, template.replace("<any>", logo_name))
73723
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    22
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    23
      Isabelle_System.bash(
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    24
        "\"$ISABELLE_EPSTOPDF\" --filter < " + File.bash_path(tmp_file) +
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    25
          " > " + File.bash_path(output_file)).check
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    26
      if (!quiet) Output.writeln(output_file.expand.implode)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    27
    }
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    28
  }
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    29
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    30
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    31
  /* Isabelle tool wrapper */
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    32
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    33
  val isabelle_tool =
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73723
diff changeset
    34
    Isabelle_Tool("logo", "create variants of the Isabelle logo (PDF)", Scala_Project.here,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    35
      { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    36
        var output: Option[Path] = None
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    37
        var quiet = false
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    38
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    39
        val getopts = Getopts("""
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    40
Usage: isabelle logo [OPTIONS] [NAME]
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    41
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    42
  Options are:
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    43
    -o FILE      alternative output file
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    44
    -q           quiet mode
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    45
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    46
  Create variant NAME of the Isabelle logo as "isabelle_name.pdf".
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    47
""",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    48
          "o:" -> (arg => output = Some(Path.explode(arg))),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    49
          "q" -> (_ => quiet = true))
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    50
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    51
        val more_args = getopts(args)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    52
        val logo_name =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    53
          more_args match {
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    54
            case Nil => ""
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    55
            case List(name) => name
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    56
            case _ => getopts.usage()
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    57
          }
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    58
        create_logo(logo_name, output getOrElse make_output_file(logo_name), quiet = quiet)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    59
      })
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    60
}