src/Pure/Thy/html.ML
changeset 6347 ce7ab97a8e15
parent 6338 bf0d22535e47
child 6361 3a45ad4a95eb
equal deleted inserted replaced
6346:643a1bd31a91 6347:ce7ab97a8e15
    25   val begin_index: Path.T * string -> Path.T * string -> Path.T option -> text
    25   val begin_index: Path.T * string -> Path.T * string -> Path.T option -> text
    26   val end_index: text
    26   val end_index: text
    27   val theory_entry: Path.T * string -> text
    27   val theory_entry: Path.T * string -> text
    28   val session_entries: (Path.T * string) list -> text
    28   val session_entries: (Path.T * string) list -> text
    29   val source: (string, 'a) Source.source -> text
    29   val source: (string, 'a) Source.source -> text
    30   val begin_theory: Path.T * string -> string -> string list -> ((Path.T * Path.T) * bool) list
    30   val begin_theory: Path.T * string -> string -> string list ->
    31     -> text -> text
    31     (Path.T option * Path.T * bool) list -> text -> text
    32   val end_theory: text
    32   val end_theory: text
    33   val ml_file: Path.T -> string -> text
    33   val ml_file: Path.T -> string -> text
    34   val theorem: string -> thm -> text
    34   val theorem: string -> thm -> text
    35   val section: string -> text
    35   val section: string -> text
    36   val setup: (theory -> theory) list
    36   val setup: (theory -> theory) list
    80 val _ = Symbol.add_mode htmlN output_width;
    80 val _ = Symbol.add_mode htmlN output_width;
    81 
    81 
    82 
    82 
    83 (* token translations *)
    83 (* token translations *)
    84 
    84 
    85 fun tagit bg en = apfst (enclose bg en) o output_width;
    85 fun color col =
    86 fun color col = tagit ("<font color=" ^ quote col ^ ">") "</font>";
    86   apfst (enclose ("<font color=" ^ quote col ^ ">") "</font>") o output_width;
    87 
    87 
    88 val html_trans =
    88 val html_trans =
    89  [("class", color "red"),
    89  [("class", color "red"),
    90   ("tfree", color "purple"),
    90   ("tfree", color "purple"),
    91   ("tvar",  color "purple"),
    91   ("tvar",  color "purple"),
   143 
   143 
   144 (* session index *)
   144 (* session index *)
   145 
   145 
   146 fun begin_index back (index_path, session) opt_readme =
   146 fun begin_index back (index_path, session) opt_readme =
   147   begin_document ("Index of " ^ session) ^ back_link back ^
   147   begin_document ("Index of " ^ session) ^ back_link back ^
   148   (case opt_readme of None => "" | Some p => para (href_path p "README" ^ " file")) ^
   148   (case opt_readme of None => "" | Some p => href_path p "README" ^ " file") ^
   149   "\n<hr>\n\n<h2>Theories</h2>\n";
   149   "\n<hr>\n\n<h2>Theories</h2>\n";
   150 
   150 
   151 val end_index = end_document;
   151 val end_index = end_document;
   152 
   152 
   153 fun entry (p, s) = href_path p (plain s) ^ "<br>\n";
   153 fun entry (p, s) = href_path p (plain s) ^ "<br>\n";
   162 fun output_source src = implode (output_symbols (Source.exhaust (Symbol.source false src)));
   162 fun output_source src = implode (output_symbols (Source.exhaust (Symbol.source false src)));
   163 fun source src = "\n<hr>\n<pre>" ^ output_source src ^ "</pre>\n<hr>\n";
   163 fun source src = "\n<hr>\n<pre>" ^ output_source src ^ "</pre>\n<hr>\n";
   164 
   164 
   165 
   165 
   166 local
   166 local
   167   fun file ((p, p'), loadit) =
   167   fun file (opt_ref, path, loadit) =
   168     href_path p' ((if not loadit then enclose "(" ")" else I) (file_path p));
   168     (case opt_ref of None => I | Some p => href_path p)
       
   169       ((if not loadit then enclose "(" ")" else I) (file_path path));
   169 
   170 
   170   fun suffix_last _ [] = []
   171   fun suffix_last _ [] = []
   171     | suffix_last s lst = let val (xs, x) = split_last lst in xs @ [x ^ s] end;
   172     | suffix_last s lst = let val (xs, x) = split_last lst in xs @ [x ^ s] end;
   172 
   173 
   173   val plus_names = space_implode " + " o map name;
   174   val plus_names = space_implode " + " o map name;