isabelle: src/Pure/Thy/html.ML@93224745477f (annotated)

24584 01e83ffa6c54 fixed title haftmann parents: 24244 diff changeset	1	(* Title: Pure/Thy/html.ML
9415 daa2296f23ea removed all_sessions; wenzelm parents: 9045 diff changeset	2	Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	3
9415 daa2296f23ea removed all_sessions; wenzelm parents: 9045 diff changeset	4	HTML presentation elements.
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	5	*)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	6
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	7	signature HTML =
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	8	sig
23724 6e95ed5f64da export html_mode, begin_document, end_document; wenzelm parents: 23703 diff changeset	9	val html_mode: ('a -> 'b) -> 'a -> 'b
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	10	val reset_symbols: unit -> unit
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	11	val init_symbols: (string * int) list -> unit
23622 8ce09f692653 simplified pretty token metric: type int; wenzelm parents: 22796 diff changeset	12	type text = string
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	13	val plain: string -> text
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	14	val name: string -> text
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	15	val keyword: string -> text
23622 8ce09f692653 simplified pretty token metric: type int; wenzelm parents: 22796 diff changeset	16	val command: string -> text
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	17	val href_name: string -> text -> text
6649 2156012be986 Reimplemented graph generator. berghofe parents: 6405 diff changeset	18	val href_path: Url.T -> text -> text
2156012be986 Reimplemented graph generator. berghofe parents: 6405 diff changeset	19	val href_opt_path: Url.T option -> text -> text
6376 c87f3769203a tuned; wenzelm parents: 6361 diff changeset	20	val para: text -> text
23724 6e95ed5f64da export html_mode, begin_document, end_document; wenzelm parents: 23703 diff changeset	21	val begin_document: string -> text
6e95ed5f64da export html_mode, begin_document, end_document; wenzelm parents: 23703 diff changeset	22	val end_document: text
59448 149d2bc5ddb6 prefer plain session_graph.pdf over GraphBrowser applet; wenzelm parents: 55041 diff changeset	23	val begin_session_index: string -> Url.T -> (Url.T * string) list -> text
6649 2156012be986 Reimplemented graph generator. berghofe parents: 6405 diff changeset	24	val theory_entry: Url.T * string -> text
54456 f4b1440d9880 simplified HTML theory presentation; wenzelm parents: 54455 diff changeset	25	val theory: string -> (Url.T option * string) list -> text -> text
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	26	end;
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	27
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	28	structure HTML: HTML =
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	29	struct
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	30
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	31
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	32	( HTML print modes )
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	33
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	34	(* mode *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	35
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	36	val htmlN = "HTML";
37146 f652333bbf8e renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time; wenzelm parents: 34003 diff changeset	37	fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	38
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	39
33985 1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	40	(* common markup *)
1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	41
1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	42	fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	43
46866 b190913c3c41 simplified span class in conformance to Scala version; wenzelm parents: 45666 diff changeset	44	val _ = Markup.add_mode htmlN (span o fst);
33985 1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	45
1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	46
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	47	(* symbol output *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	48
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	49	local
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	50
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	51	val hidden = span Markup.hiddenN \|-> enclose;
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	52
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	53	val symbols =
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	54	Synchronized.var "HTML.symbols" (NONE: (int * string) Symtab.table option);
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	55
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	56	fun output_sym s =
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	57	if Symbol.is_raw s then (1, Symbol.decode_raw s)
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	58	else
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	59	(case Synchronized.value symbols of
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	60	SOME tab =>
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	61	(case Symtab.lookup tab s of
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	62	SOME x => x
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	63	\| NONE => (size s, XML.text s))
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	64	\| NONE => raise Fail "Missing HTML.init_symbols: cannot output symbols");
33985 1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	65
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	66	fun output_markup (bg, en) s1 s2 =
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	67	let val (n, txt) = output_sym s2
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	68	in (n, hidden s1 ^ enclose bg en txt) end;
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	69
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	70	val output_sub = output_markup ("<sub>", "</sub>");
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	71	val output_sup = output_markup ("<sup>", "</sup>");
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	72	val output_bold = output_markup (span "bold");
17178 18a98ecc6821 output \<^loc> as 'loc' span; wenzelm parents: 17116 diff changeset	73
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	74	fun output_syms [] (result, width) = (implode (rev result), width)
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	75	\| output_syms (s1 :: rest) (result, width) =
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	76	let
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	77	val (s2, ss) = (case rest of [] => ("", []) \| s2 :: ss => (s2, ss));
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	78	val ((w, s), r) =
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	79	if s1 = "\\<^sub>" then (output_sub "⇩" s2, ss)
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	80	else if s1 = "\\<^sup>" then (output_sup "⇧" s2, ss)
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	81	else if s1 = "\\<^bold>" then (output_bold "❙" s2, ss)
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	82	else (output_sym s1, rest);
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	83	in output_syms r (s :: result, width + w) end;
14534 7a46bdcd92f2 treat sub/super scripts kleing parents: 14083 diff changeset	84
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	85	in
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	86
41482 f4c07fdd1d48 more scalable HTML.output_width; wenzelm parents: 40946 diff changeset	87	fun output_width str = output_syms (Symbol.explode str) ([], 0);
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	88	val output = #1 o output_width;
bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	89
26709 f963ea18a579 replaced token translations by common markup; wenzelm parents: 26463 diff changeset	90	val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
f963ea18a579 replaced token translations by common markup; wenzelm parents: 26463 diff changeset	91
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	92
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	93	fun reset_symbols () = Synchronized.change symbols (K NONE);
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	94
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	95	fun init_symbols codes =
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	96	let
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	97	val mapping =
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	98	map (fn (s, c) => (s, (Symbol.length [s], "&#" ^ Markup.print_int c ^ ";"))) codes @
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	99	[("", (0, "")),
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	100	("'", (1, "'")),
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	101	("\\<^bsub>", (0, hidden "⇘" ^ "<sub>")),
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	102	("\\<^esub>", (0, hidden "⇙" ^ "</sub>")),
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	103	("\\<^bsup>", (0, hidden "⇗" ^ "<sup>")),
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	104	("\\<^esup>", (0, hidden "⇖" ^ "</sup>"))];
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	105	in Synchronized.change symbols (K (SOME (fold Symtab.update mapping Symtab.empty))) end;
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	106
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	107	end;
bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	108
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	109
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	110
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	111	( HTML markup )
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	112
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	113	type text = string;
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	114
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	115
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	116	(* atoms *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	117
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	118	val plain = output;
19265 cae36e16f3c0 Output.add_mode: keyword component; wenzelm parents: 18708 diff changeset	119	val name = enclose "<span class=\"name\">" "</span>" o output;
cae36e16f3c0 Output.add_mode: keyword component; wenzelm parents: 18708 diff changeset	120	val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
23622 8ce09f692653 simplified pretty token metric: type int; wenzelm parents: 22796 diff changeset	121	val command = enclose "<span class=\"command\">" "</span>" o output;
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	122
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	123
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	124	(* misc *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	125
28840 049f0a8faa35 tuned; wenzelm parents: 27896 diff changeset	126	fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
21858 05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert; wenzelm parents: 20742 diff changeset	127	fun href_path path txt = href_name (Url.implode path) txt;
6376 c87f3769203a tuned; wenzelm parents: 6361 diff changeset	128
15531 08c8dad8e399 Deleted Library.option type. skalberg parents: 15336 diff changeset	129	fun href_opt_path NONE txt = txt
08c8dad8e399 Deleted Library.option type. skalberg parents: 15336 diff changeset	130	\| href_opt_path (SOME p) txt = href_path p txt;
6376 c87f3769203a tuned; wenzelm parents: 6361 diff changeset	131
12413 f879fcc9412d tuned line breaks in HTML source; wenzelm parents: 12151 diff changeset	132	fun para txt = "\n<p>" ^ txt ^ "</p>\n";
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	133
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	134
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	135	(* document *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	136
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	137	fun begin_document title =
40946 3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	138	"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	139	\<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	140	\\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	141	\<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	142	\<head>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	143	\<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	144	\<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	145	\<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	146	\</head>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	147	\\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	148	\<body>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	149	\<div class=\"head\">\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8; wenzelm parents: 39616 diff changeset	150	\<h1>" ^ plain title ^ "</h1>\n";
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	151
14541 0a7743e2f8dd use css kleing parents: 14534 diff changeset	152	val end_document = "\n</div>\n</body>\n</html>\n";
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	153
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	154
bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	155	(* session index *)
bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	156
59448 149d2bc5ddb6 prefer plain session_graph.pdf over GraphBrowser applet; wenzelm parents: 55041 diff changeset	157	fun begin_session_index session graph docs =
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50233 diff changeset	158	begin_document ("Session " ^ plain session) ^
6754 c23c542a32e5 tuned markup; wenzelm parents: 6649 diff changeset	159	para ("View " ^ href_path graph "theory dependencies" ^
27829 c073006e0137 produce XHTML 1.0 Transitional; wenzelm parents: 27490 diff changeset	160	implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
37941 1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well; wenzelm parents: 37940 diff changeset	161	"\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	162
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50233 diff changeset	163	fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	164
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	165
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	166	(* theory *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	167
54456 f4b1440d9880 simplified HTML theory presentation; wenzelm parents: 54455 diff changeset	168	fun theory A Bs txt =
f4b1440d9880 simplified HTML theory presentation; wenzelm parents: 54455 diff changeset	169	begin_document ("Theory " ^ A) ^ "\n" ^
f4b1440d9880 simplified HTML theory presentation; wenzelm parents: 54455 diff changeset	170	command "theory" ^ " " ^ name A ^ "<br/>\n" ^
54455 1d977436c1bf removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013; wenzelm parents: 53194 diff changeset	171	keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
54456 f4b1440d9880 simplified HTML theory presentation; wenzelm parents: 54455 diff changeset	172	"<br/>\n" ^
61374 b3c665940d62 server-side fonts; wenzelm parents: 59448 diff changeset	173	enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^
54456 f4b1440d9880 simplified HTML theory presentation; wenzelm parents: 54455 diff changeset	174	end_document;
16267 0773b17922d8 present new-style theory header, with 'imports' and 'uses'; wenzelm parents: 16196 diff changeset	175
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	176	end;

author	wenzelm
	Fri, 09 Oct 2015 19:25:13 +0200
changeset 61376	93224745477f
parent 61374	b3c665940d62
child 61379	c57820ceead3
permissions	-rw-r--r--