src/Pure/Tools/logo.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73723 1bbbaae6b5e3
child 75394 42267c650205
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
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 = {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73723
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)
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    27
    })
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,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73723
diff changeset
    35
      args => {
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    36
      var output: Option[Path] = None
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    37
      var quiet = false
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    38
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    39
      val getopts = Getopts("""
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
""",
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    48
        "o:" -> (arg => output = Some(Path.explode(arg))),
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    49
        "q" -> (_ => quiet = true))
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    50
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    51
      val more_args = getopts(args)
73723
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    52
      val logo_name =
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    53
        more_args match {
73723
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    54
          case Nil => ""
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    55
          case List(name) => name
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    56
          case _ => getopts.usage()
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    57
        }
73723
1bbbaae6b5e3 option document_logo;
wenzelm
parents: 73399
diff changeset
    58
      create_logo(logo_name, output getOrElse make_output_file(logo_name), quiet = quiet)
73399
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    59
    })
48569c862eb8 proper Isabelle/Scala tool --- avoid perl;
wenzelm
parents:
diff changeset
    60
}