src/Pure/Thy/present.ML
author wenzelm
Tue, 17 Nov 2020 16:48:18 +0100
changeset 72635 2a329baa7d39
parent 72622 830222403681
child 72636 09ee9eb7a3d3
permissions -rw-r--r--
proper link location;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/present.ML
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
     2
    Author:     Makarius
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     3
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
     4
Theory presentation: HTML and LaTeX documents.
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     5
*)
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     6
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     7
signature PRESENT =
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     8
sig
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
     9
  val document_html_name: theory -> Path.binding
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    10
  val document_tex_name: theory -> Path.binding
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    11
  val html_name: theory -> Path.T
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    12
  val export_html: theory -> Command_Span.span list -> unit
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    13
end;
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    14
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    15
structure Present: PRESENT =
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    16
struct
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    17
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    18
(** artefact names **)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    19
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    20
fun document_name ext thy =
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    21
  Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    22
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    23
val document_html_name = document_name "html";
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    24
val document_tex_name = document_name "tex";
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    25
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    26
fun html_name thy = Path.basic (Context.theory_name thy ^ ".html");
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    27
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    28
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    29
(* theory as HTML *)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    30
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    31
local
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    32
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    33
fun get_session_chapter thy =
59448
149d2bc5ddb6 prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents: 59446
diff changeset
    34
  let
72616
217e6cf61453 refer to session structure from resources;
wenzelm
parents: 72613
diff changeset
    35
    val session = Resources.theory_qualifier (Context.theory_long_name thy);
217e6cf61453 refer to session structure from resources;
wenzelm
parents: 72613
diff changeset
    36
    val chapter = Resources.session_chapter session;
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    37
  in (session, chapter) end;
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    38
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    39
fun theory_link thy thy' =
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    40
  let
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    41
    val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy');
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    42
    val link = html_name thy';
59448
149d2bc5ddb6 prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents: 59446
diff changeset
    43
  in
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    44
    if session = session' then SOME link
72635
2a329baa7d39 proper link location;
wenzelm
parents: 72622
diff changeset
    45
    else if chapter = chapter' then SOME (Path.parent + Path.basic session' + link)
2a329baa7d39 proper link location;
wenzelm
parents: 72622
diff changeset
    46
    else if chapter' = Context.PureN then NONE
2a329baa7d39 proper link location;
wenzelm
parents: 72622
diff changeset
    47
    else SOME (Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link)
59448
149d2bc5ddb6 prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents: 59446
diff changeset
    48
  end;
149d2bc5ddb6 prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents: 59446
diff changeset
    49
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    50
fun theory_document symbols A Bs body =
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    51
  HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    52
  HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    53
  HTML.keyword symbols "imports" ^ " " ^
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    54
    space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    55
  "<br/>\n\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    56
  body @ ["</pre>\n", HTML.end_document];
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    57
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    58
in
54456
f4b1440d9880 simplified HTML theory presentation;
wenzelm
parents: 54455
diff changeset
    59
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    60
fun export_html thy spans =
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    61
  let
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    62
    val name = Context.theory_name thy;
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    63
    val parents =
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    64
      Theory.parents_of thy |> map (fn thy' =>
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    65
        (Option.map Url.File (theory_link thy thy'), Context.theory_name thy'));
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72511
diff changeset
    66
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    67
    val symbols = Resources.html_symbols ();
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    68
    val keywords = Thy_Header.get_keywords thy;
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    69
    val body = map (HTML.present_span symbols keywords) spans;
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    70
    val html = XML.blob (theory_document symbols name parents body);
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    71
  in Export.export thy (document_html_name thy) html end
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    72
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    73
end;
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    74
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72620
diff changeset
    75
end;