src/Pure/Admin/build_doc.scala
author wenzelm
Sun, 13 Dec 2020 13:46:28 +0100
changeset 72897 86eff7a823f3
parent 72854 6c660f05f70c
child 73340 0ffcad1f6130
permissions -rw-r--r--
tuned messages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
     1
/*  Title:      Pure/Admin/build_doc.scala
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     3
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     4
Build Isabelle documentation.
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     5
*/
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     6
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     8
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     9
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    10
object Build_Doc
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    11
{
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    12
  /* build_doc */
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    13
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    14
  def build_doc(
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    15
    options: Options,
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 69854
diff changeset
    16
    progress: Progress = new Progress,
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    17
    all_docs: Boolean = false,
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    18
    max_jobs: Int = 1,
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    19
    docs: List[String] = Nil)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    20
  {
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    21
    val store = Sessions.store(options)
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    22
67026
687c822ee5e3 tuned signature;
wenzelm
parents: 67023
diff changeset
    23
    val sessions_structure = Sessions.load_structure(options)
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    24
    val selected =
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    25
      for {
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    26
        session <- sessions_structure.build_topological_order
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    27
        info = sessions_structure(session)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    28
        if info.groups.contains("doc")
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    29
        doc = info.options.string("document_variants")
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    30
        if all_docs || docs.contains(doc)
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    31
      } yield (doc, session)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    32
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    33
    val documents = selected.map(_._1)
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    34
    val selection = Sessions.Selection(sessions = selected.map(_._2))
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    35
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    36
    docs.filter(doc => !documents.contains(doc)) match {
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    37
      case Nil =>
56432
wenzelm
parents: 56430
diff changeset
    38
      case bad => error("No documentation session for " + commas_quote(bad))
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    39
    }
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    40
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    41
    progress.echo("Build started for sessions " + commas_quote(selection.sessions))
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    42
    Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).ok ||
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    43
      error("Build failed")
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    44
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    45
    progress.echo("Build started for documentation " + commas_quote(documents))
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    46
    val doc_options = options + "document=pdf"
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    47
    val deps = Sessions.load_structure(doc_options).selection_deps(selection)
72597
e8d7dc1c229c more parallelism;
wenzelm
parents: 72594
diff changeset
    48
e8d7dc1c229c more parallelism;
wenzelm
parents: 72594
diff changeset
    49
    val errs =
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    50
      Par_List.map[(String, String), Option[String]](
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    51
      {
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    52
        case (doc, session) =>
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    53
          try {
72897
86eff7a823f3 tuned messages;
wenzelm
parents: 72854
diff changeset
    54
            progress.echo("Documentation " + quote(doc) + " ...")
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72675
diff changeset
    55
72854
6c660f05f70c clarified signature;
wenzelm
parents: 72763
diff changeset
    56
            using(store.open_database_context())(db_context =>
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72675
diff changeset
    57
              Presentation.build_documents(session, deps, db_context,
72685
a7877e14e7f8 proper output directory (amending cc1347c8c804);
wenzelm
parents: 72683
diff changeset
    58
                output_pdf = Some(Path.explode("~~/doc"))))
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    59
            None
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    60
          }
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    61
          catch {
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    62
            case Exn.Interrupt.ERROR(msg) =>
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    63
              val sep = if (msg.contains('\n')) "\n" else " "
72897
86eff7a823f3 tuned messages;
wenzelm
parents: 72854
diff changeset
    64
              Some("Documentation " + quote(doc) + " failed:" + sep + msg)
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    65
          }
cc1347c8c804 clarified document output;
wenzelm
parents: 72652
diff changeset
    66
      }, selected).flatten
72597
e8d7dc1c229c more parallelism;
wenzelm
parents: 72594
diff changeset
    67
e8d7dc1c229c more parallelism;
wenzelm
parents: 72594
diff changeset
    68
    if (errs.nonEmpty) error(cat_lines(errs))
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    69
  }
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    70
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    71
62838
c91ca9935280 prefer internal tool;
wenzelm
parents: 62641
diff changeset
    72
  /* Isabelle tool wrapper */
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    73
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    74
  val isabelle_tool =
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72685
diff changeset
    75
    Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here, args =>
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    76
    {
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    77
      var all_docs = false
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    78
      var max_jobs = 1
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69277
diff changeset
    79
      var options = Options.init()
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    80
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    81
      val getopts =
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    82
        Getopts("""
64310
wenzelm
parents: 64220
diff changeset
    83
Usage: isabelle build_doc [OPTIONS] [DOCS ...]
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    84
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    85
  Options are:
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    86
    -a           select all documentation sessions
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    87
    -j INT       maximum number of parallel jobs (default 1)
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69277
diff changeset
    88
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    89
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    90
  Build Isabelle documentation from documentation sessions with
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    91
  suitable document_variants entry.
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    92
""",
64310
wenzelm
parents: 64220
diff changeset
    93
          "a" -> (_ => all_docs = true),
wenzelm
parents: 64220
diff changeset
    94
          "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69277
diff changeset
    95
          "o:" -> (arg => options = options + arg))
62838
c91ca9935280 prefer internal tool;
wenzelm
parents: 62641
diff changeset
    96
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    97
      val docs = getopts(args)
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    98
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    99
      if (!all_docs && docs.isEmpty) getopts.usage()
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
   100
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
   101
      val progress = new Console_Progress()
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
   102
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
   103
      progress.interrupt_handler {
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
   104
        build_doc(options, progress, all_docs, max_jobs, docs)
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
   105
      }
69277
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 67026
diff changeset
   106
    })
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
   107
}