src/Pure/Admin/build_doc.scala
author wenzelm
Tue Nov 07 15:45:33 2017 +0100 (17 months ago)
changeset 67023 e27e05d6f2a7
parent 65519 d244d8f8e13f
child 67026 687c822ee5e3
permissions -rw-r--r--
tuned signature;
wenzelm@64161
     1
/*  Title:      Pure/Admin/build_doc.scala
wenzelm@56429
     2
    Author:     Makarius
wenzelm@56429
     3
wenzelm@56429
     4
Build Isabelle documentation.
wenzelm@56429
     5
*/
wenzelm@56429
     6
wenzelm@56429
     7
package isabelle
wenzelm@56429
     8
wenzelm@56429
     9
wenzelm@56429
    10
import java.io.{File => JFile}
wenzelm@56429
    11
wenzelm@56429
    12
wenzelm@56429
    13
object Build_Doc
wenzelm@56429
    14
{
wenzelm@56429
    15
  /* build_doc */
wenzelm@56429
    16
wenzelm@56429
    17
  def build_doc(
wenzelm@56429
    18
    options: Options,
wenzelm@64909
    19
    progress: Progress = No_Progress,
wenzelm@56429
    20
    all_docs: Boolean = false,
wenzelm@56429
    21
    max_jobs: Int = 1,
wenzelm@56429
    22
    system_mode: Boolean = false,
wenzelm@56429
    23
    docs: List[String] = Nil): Int =
wenzelm@56429
    24
  {
wenzelm@67023
    25
    val sessions_structure = Sessions.load(options)
wenzelm@56429
    26
    val selection =
wenzelm@56429
    27
      for {
wenzelm@67023
    28
        name <- sessions_structure.build_topological_order
wenzelm@67023
    29
        info = sessions_structure(name)
wenzelm@56429
    30
        if info.groups.contains("doc")
wenzelm@56429
    31
        doc = info.options.string("document_variants")
wenzelm@56429
    32
        if all_docs || docs.contains(doc)
wenzelm@67023
    33
      } yield (doc, name)
wenzelm@56429
    34
wenzelm@56429
    35
    val selected_docs = selection.map(_._1)
wenzelm@56429
    36
    val sessions = selection.map(_._2)
wenzelm@56429
    37
wenzelm@56429
    38
    docs.filter(doc => !selected_docs.contains(doc)) match {
wenzelm@56429
    39
      case Nil =>
wenzelm@56432
    40
      case bad => error("No documentation session for " + commas_quote(bad))
wenzelm@56429
    41
    }
wenzelm@56429
    42
wenzelm@56432
    43
    progress.echo("Build started for documentation " + commas_quote(selected_docs))
wenzelm@56429
    44
wenzelm@62641
    45
    val res1 =
wenzelm@56429
    46
      Build.build(options, progress, requirements = true, build_heap = true,
wenzelm@56429
    47
        max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
wenzelm@62641
    48
    if (res1.ok) {
wenzelm@56429
    49
      Isabelle_System.with_tmp_dir("document_output")(output =>
wenzelm@56429
    50
        {
wenzelm@62641
    51
          val res2 =
wenzelm@56429
    52
            Build.build(
wenzelm@56429
    53
              options.bool.update("browser_info", false).
wenzelm@56429
    54
                string.update("document", "pdf").
wenzelm@64220
    55
                string.update("document_output", output.implode),
wenzelm@56430
    56
              progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
wenzelm@56430
    57
              sessions = sessions)
wenzelm@62641
    58
          if (res2.ok) {
wenzelm@65082
    59
            val doc_dir = Path.explode("~~/doc")
wenzelm@56429
    60
            for (doc <- selected_docs) {
wenzelm@64220
    61
              val name = Path.explode(doc + ".pdf")
wenzelm@64220
    62
              File.copy(output + name, doc_dir + name)
wenzelm@56429
    63
            }
wenzelm@56429
    64
          }
wenzelm@62641
    65
          res2.rc
wenzelm@56429
    66
        })
wenzelm@56429
    67
    }
wenzelm@62641
    68
    else res1.rc
wenzelm@56429
    69
  }
wenzelm@56429
    70
wenzelm@56429
    71
wenzelm@62838
    72
  /* Isabelle tool wrapper */
wenzelm@56429
    73
wenzelm@64161
    74
  val isabelle_tool =
wenzelm@64161
    75
    Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
wenzelm@64161
    76
    {
wenzelm@64161
    77
      var all_docs = false
wenzelm@64161
    78
      var max_jobs = 1
wenzelm@64161
    79
      var system_mode = false
wenzelm@62435
    80
wenzelm@64161
    81
      val getopts =
wenzelm@64161
    82
        Getopts("""
wenzelm@64310
    83
Usage: isabelle build_doc [OPTIONS] [DOCS ...]
wenzelm@62435
    84
wenzelm@62435
    85
  Options are:
wenzelm@62435
    86
    -a           select all documentation sessions
wenzelm@62435
    87
    -j INT       maximum number of parallel jobs (default 1)
wenzelm@62435
    88
    -s           system build mode
wenzelm@62435
    89
wenzelm@62435
    90
  Build Isabelle documentation from documentation sessions with
wenzelm@62435
    91
  suitable document_variants entry.
wenzelm@62435
    92
""",
wenzelm@64310
    93
          "a" -> (_ => all_docs = true),
wenzelm@64310
    94
          "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
wenzelm@64310
    95
          "s" -> (_ => system_mode = true))
wenzelm@62838
    96
wenzelm@64161
    97
      val docs = getopts(args)
wenzelm@62435
    98
wenzelm@64161
    99
      if (!all_docs && docs.isEmpty) getopts.usage()
wenzelm@62435
   100
wenzelm@64161
   101
      val options = Options.init()
wenzelm@64161
   102
      val progress = new Console_Progress()
wenzelm@64161
   103
      val rc =
wenzelm@64161
   104
        progress.interrupt_handler {
wenzelm@64161
   105
          build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
wenzelm@64161
   106
        }
wenzelm@64161
   107
      sys.exit(rc)
wenzelm@64161
   108
    }, admin = true)
wenzelm@56429
   109
}