# HG changeset patch # User wenzelm # Date 1605912454 -3600 # Node ID 5e7916535860f9b9b6b4c05a179aa3f7043ebe4b # Parent b1388cfb64bb65d4078aa4a04998ad2eec5e0577 generate theory HTML in Isabelle/Scala; discontinued HTML support in Isabelle/ML; diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/Isar/keyword.scala Fri Nov 20 23:47:34 2020 +0100 @@ -88,6 +88,9 @@ PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) + val proof_asm = Set(PRF_ASM, PRF_ASM_GOAL) + val improper = Set(QED_SCRIPT, PRF_SCRIPT, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) + val theory_goal = Set(THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT) val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) val qed = Set(QED, QED_SCRIPT, QED_BLOCK) diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/Isar/token.scala Fri Nov 20 23:47:34 2020 +0100 @@ -328,6 +328,8 @@ def is_end: Boolean = is_command("end") def is_begin_or_command: Boolean = is_begin || is_command + def symbol_length: Symbol.Offset = Symbol.iterator(source).length + def content: String = if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source) else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source) diff -r b1388cfb64bb -r 5e7916535860 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/PIDE/document.scala Fri Nov 20 23:47:34 2020 +0100 @@ -86,6 +86,9 @@ abbrevs: Thy_Header.Abbrevs = Nil, errors: List[String] = Nil) { + def imports_offset: Map[Int, Name] = + (for { (name, Position.Offset(i)) <- imports_pos } yield i -> name).toMap + def imports: List[Name] = imports_pos.map(_._1) def append_errors(msgs: List[String]): Header = diff -r b1388cfb64bb -r 5e7916535860 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/PIDE/resources.ML Fri Nov 20 23:47:34 2020 +0100 @@ -8,8 +8,7 @@ sig val default_qualifier: string val init_session: - {html_symbols: (string * int) list, - session_positions: (string * Properties.T) list, + {session_positions: (string * Properties.T) list, session_directories: (string * string) list, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, @@ -22,7 +21,6 @@ val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool - val html_symbols: unit -> HTML.symbols val check_session: Proof.context -> string * Position.T -> string val session_chapter: string -> string val last_timing: Toplevel.transition -> Time.time @@ -97,8 +95,7 @@ {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = - {html_symbols = HTML.no_symbols, - session_positions = []: (string * entry) list, + {session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, session_chapters = Symtab.empty: string Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, @@ -111,12 +108,11 @@ Synchronized.var "Sessions.base" empty_session_base; fun init_session - {html_symbols, session_positions, session_directories, session_chapters, + {session_positions, session_directories, session_chapters, bibtex_entries, command_timings, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => - {html_symbols = HTML.make_symbols html_symbols, - session_positions = sort_by #1 (map (apsnd make_entry) session_positions), + {session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, @@ -129,20 +125,18 @@ fun init_session_yxml yxml = let - val (html_symbols, (session_positions, (session_directories, (session_chapters, - (bibtex_entries, (command_timings, (docs, (global_theories, loaded_theories)))))))) = + val (session_positions, (session_directories, (session_chapters, + (bibtex_entries, (command_timings, (docs, (global_theories, loaded_theories))))))) = YXML.parse_body yxml |> let open XML.Decode in - pair (list (pair string int)) - (pair (list (pair string properties)) - (pair (list (pair string string)) (pair (list (pair string string)) - (pair (list (pair string (list string))) (pair (list properties) - (pair (list string) (pair (list (pair string string)) (list string)))))))) + (pair (list (pair string properties)) + (pair (list (pair string string)) (pair (list (pair string string)) + (pair (list (pair string (list string))) (pair (list properties) + (pair (list string) (pair (list (pair string string)) (list string)))))))) end; in init_session - {html_symbols = html_symbols, - session_positions = session_positions, + {session_positions = session_positions, session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, @@ -158,8 +152,7 @@ fun finish_session_base () = Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => - {html_symbols = HTML.no_symbols, - session_positions = [], + {session_positions = [], session_directories = Symtab.empty, session_chapters = Symtab.empty, bibtex_entries = Symtab.empty, @@ -173,8 +166,6 @@ fun global_theory a = Symtab.lookup (get_session_base #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; -fun html_symbols () = get_session_base #html_symbols; - fun check_name which kind markup ctxt arg = Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt arg; diff -r b1388cfb64bb -r 5e7916535860 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/PIDE/resources.scala Fri Nov 20 23:47:34 2020 +0100 @@ -28,15 +28,13 @@ import XML.Encode._ YXML.string_of_body( - pair(list(pair(string, int)), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(pair(string, string)), pair(list(pair(string, list(string))), pair(list(properties), pair(list(string), - pair(list(pair(string, string)), list(string)))))))))( - (Symbol.codes, + pair(list(pair(string, string)), list(string))))))))( (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.session_chapters, @@ -44,7 +42,7 @@ (command_timings, (session_base.doc_names, (session_base.global_theories.toList, - session_base.loaded_theories.keys)))))))))) + session_base.loaded_theories.keys))))))))) } diff -r b1388cfb64bb -r 5e7916535860 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/ROOT.ML Fri Nov 20 23:47:34 2020 +0100 @@ -232,7 +232,6 @@ ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; -ML_file "Thy/html.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Fri Nov 20 14:29:21 2020 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* Title: Pure/Thy/html.ML - Author: Makarius - -HTML presentation elements. -*) - -signature HTML = -sig - type symbols - val make_symbols: (string * int) list -> symbols - val no_symbols: symbols - val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output - type text = string - val name: symbols -> string -> text - val keyword: symbols -> string -> text - val command: symbols -> string -> text - val href_name: string -> string -> string - val href_path: Url.T -> string -> string - val begin_document: symbols -> string -> text - val end_document: text -end; - -structure HTML: HTML = -struct - - -(* common markup *) - -fun span "" = ("", "") - | span class = ("", ""); - -val enclose_span = uncurry enclose o span; - -val hidden = enclose_span Markup.hiddenN; - - -(* symbol output *) - -abstype symbols = Symbols of string Symtab.table -with - -fun make_symbols codes = - let - val mapping = - map (apsnd (fn c => "" ^ Value.print_int c ^ ";")) codes @ - [("'", "'"), - ("\<^bsub>", hidden "⇘" ^ ""), - ("\<^esub>", hidden "⇙" ^ ""), - ("\<^bsup>", hidden "⇗" ^ ""), - ("\<^esup>", hidden "⇖" ^ "")]; - in Symbols (fold Symtab.update mapping Symtab.empty) end; - -val no_symbols = make_symbols []; - -fun output_sym (Symbols tab) s = - (case Symtab.lookup tab s of - SOME x => x - | NONE => XML.text s); - -end; - -local - -fun output_markup (bg, en) symbols s1 s2 = - hidden s1 ^ enclose bg en (output_sym symbols s2); - -val output_sub = output_markup ("", ""); -val output_sup = output_markup ("", ""); -val output_bold = output_markup (span "bold"); - -fun output_syms _ [] result = implode (rev result) - | output_syms symbols (s1 :: rest) result = - let - val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)); - val (s, r) = - if s1 = "\<^sub>" then (output_sub symbols "⇩" s2, ss) - else if s1 = "\<^sup>" then (output_sup symbols "⇧" s2, ss) - else if s1 = "\<^bold>" then (output_bold symbols "❙" s2, ss) - else (output_sym symbols s1, rest); - in output_syms symbols r (s :: result) end; - -in - -fun output symbols str = output_syms symbols (Symbol.explode str) []; - -end; - - -(* presentation *) - -fun present_span symbols keywords = - let - fun present_markup (name, props) = - (case Properties.get props Markup.kindN of - SOME kind => - if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I - | NONE => I) #> enclose_span name; - fun present_token tok = - fold_rev present_markup (Token.markups keywords tok) - (output symbols (Token.unparse tok)); - in implode o map present_token o Command_Span.content end; - - - -(** HTML markup **) - -type text = string; - - -(* atoms *) - -val name = enclose "" "" oo output; -val keyword = enclose "" "" oo output; -val command = enclose "" "" oo output; - - -(* misc *) - -fun href_name s txt = "" ^ txt ^ ""; -fun href_path path txt = href_name (Url.implode path) txt; - - -(* document *) - -fun begin_document symbols title = - XML.header ^ - "\n" ^ - "\n" ^ - "
\n" ^ - "\n" ^ - "" :: - body @ ["\n", HTML.end_document]; - -in - -fun export_html thy spans = - let - val name = Context.theory_name thy; - val parents = - Theory.parents_of thy |> map (fn thy' => - (Url.File (theory_link thy thy'), Context.theory_name thy')); - - val symbols = Resources.html_symbols (); - val keywords = Thy_Header.get_keywords thy; - val body = map (HTML.present_span symbols keywords) spans; - val html = XML.blob (theory_document symbols name parents body); - in Export.export thy (document_html_name thy) html end - -end; - (* hook for consolidated theory *) @@ -113,7 +62,6 @@ val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => - (export_html thy (map #span segments); if exists (Toplevel.is_skipped_proof o #state) segments then () else let @@ -128,7 +76,7 @@ val latex = Latex.isabelle_body thy_name body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; in Export.export thy document_tex_name (XML.blob output) end - end))); + end));