src/Pure/Tools/build_doc.scala
author wenzelm
Tue Sep 29 13:54:04 2015 +0200 (2015-09-29)
changeset 61276 8a4bd05c1735
parent 60992 89effcb342df
child 62435 2c390ad93bc8
permissions -rw-r--r--
clarified modules;
wenzelm@56429
     1
/*  Title:      Pure/Tools/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@61276
    19
    progress: Progress = Ignore_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@56429
    25
    val selection =
wenzelm@56429
    26
      for {
wenzelm@56890
    27
        (name, info) <- Build.find_sessions(options).topological_order
wenzelm@56429
    28
        if info.groups.contains("doc")
wenzelm@56429
    29
        doc = info.options.string("document_variants")
wenzelm@56429
    30
        if all_docs || docs.contains(doc)
wenzelm@56429
    31
      } yield (doc, name)
wenzelm@56429
    32
wenzelm@56429
    33
    val selected_docs = selection.map(_._1)
wenzelm@56429
    34
    val sessions = selection.map(_._2)
wenzelm@56429
    35
wenzelm@56429
    36
    docs.filter(doc => !selected_docs.contains(doc)) match {
wenzelm@56429
    37
      case Nil =>
wenzelm@56432
    38
      case bad => error("No documentation session for " + commas_quote(bad))
wenzelm@56429
    39
    }
wenzelm@56429
    40
wenzelm@56432
    41
    progress.echo("Build started for documentation " + commas_quote(selected_docs))
wenzelm@56429
    42
wenzelm@56429
    43
    val rc1 =
wenzelm@56429
    44
      Build.build(options, progress, requirements = true, build_heap = true,
wenzelm@56429
    45
        max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
wenzelm@56429
    46
    if (rc1 == 0) {
wenzelm@56429
    47
      Isabelle_System.with_tmp_dir("document_output")(output =>
wenzelm@56429
    48
        {
wenzelm@56429
    49
          val rc2 =
wenzelm@56429
    50
            Build.build(
wenzelm@56429
    51
              options.bool.update("browser_info", false).
wenzelm@56429
    52
                string.update("document", "pdf").
wenzelm@60992
    53
                string.update("document_output", File.standard_path(output)),
wenzelm@56430
    54
              progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
wenzelm@56430
    55
              sessions = sessions)
wenzelm@56429
    56
          if (rc2 == 0) {
wenzelm@56429
    57
            val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
wenzelm@56429
    58
            for (doc <- selected_docs) {
wenzelm@56429
    59
              val name = doc + ".pdf"
wenzelm@56429
    60
              File.copy(new JFile(output, name), new JFile(doc_dir, name))
wenzelm@56429
    61
            }
wenzelm@56429
    62
          }
wenzelm@56429
    63
          rc2
wenzelm@56429
    64
        })
wenzelm@56429
    65
    }
wenzelm@56429
    66
    else rc1
wenzelm@56429
    67
  }
wenzelm@56429
    68
wenzelm@56429
    69
wenzelm@56429
    70
  /* command line entry point */
wenzelm@56429
    71
wenzelm@56429
    72
  def main(args: Array[String])
wenzelm@56429
    73
  {
wenzelm@56429
    74
    Command_Line.tool {
wenzelm@56429
    75
      args.toList match {
wenzelm@56429
    76
        case
wenzelm@56429
    77
          Properties.Value.Boolean(all_docs) ::
wenzelm@56429
    78
          Properties.Value.Int(max_jobs) ::
wenzelm@56429
    79
          Properties.Value.Boolean(system_mode) ::
wenzelm@56429
    80
          Command_Line.Chunks(docs) =>
wenzelm@56429
    81
            val options = Options.init()
wenzelm@61276
    82
            val progress = new Console_Progress()
wenzelm@56429
    83
            progress.interrupt_handler {
wenzelm@56429
    84
              build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
wenzelm@56429
    85
            }
wenzelm@56429
    86
        case _ => error("Bad arguments:\n" + cat_lines(args))
wenzelm@56429
    87
      }
wenzelm@56429
    88
    }
wenzelm@56429
    89
  }
wenzelm@56429
    90
}
wenzelm@56429
    91