diff --git a/src/Pure/General/buffer.ML b/src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML
+++ b/src/Pure/General/buffer.ML
@@ -1,41 +1,46 @@
(* Title: Pure/General/buffer.ML
Author: Makarius
Scalable text buffers.
*)
signature BUFFER =
sig
type T
val empty: T
val is_empty: T -> bool
+ val add: string -> T -> T
val content: T -> string
- val add: string -> T -> T
+ val build: (T -> T) -> T
+ val build_content: (T -> T) -> string
val output: T -> (string -> unit) -> unit
val markup: Markup.T -> (T -> T) -> T -> T
end;
structure Buffer: BUFFER =
struct
abstype T = Buffer of string list
with
val empty = Buffer [];
fun is_empty (Buffer xs) = null xs;
fun add "" buf = buf
| add x (Buffer xs) = Buffer (x :: xs);
fun content (Buffer xs) = implode (rev xs);
+fun build (f: T -> T) = f empty;
+fun build_content f = build f |> content;
+
fun output (Buffer xs) out = List.app out (rev xs);
end;
fun markup m body =
let val (bg, en) = Markup.output m
in add bg #> body #> add en end;
end;
diff --git a/src/Pure/General/pretty.ML b/src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML
+++ b/src/Pure/General/pretty.ML
@@ -1,427 +1,427 @@
(* Title: Pure/General/pretty.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Markus Wenzel, TU Munich
Generic pretty printing module.
Loosely based on
D. C. Oppen, "Pretty Printing",
ACM Transactions on Programming Languages and Systems (1980), 465-483.
The object to be printed is given as a tree with indentation and line
breaking information. A "break" inserts a newline if the text until
the next break is too long to fit on the current line. After the newline,
text is indented to the level of the enclosing block. Normally, if a block
is broken then all enclosing blocks will also be broken.
The stored length of a block is used in break_dist (to treat each inner block as
a unit for breaking).
*)
signature PRETTY =
sig
val default_indent: string -> int -> Output.output
val add_mode: string -> (string -> int -> Output.output) -> unit
type T
val make_block: {markup: Markup.output, consistent: bool, indent: int} ->
T list -> T
val markup_block: {markup: Markup.T, consistent: bool, indent: int} -> T list -> T
val str: string -> T
val brk: int -> T
val brk_indent: int -> int -> T
val fbrk: T
val breaks: T list -> T list
val fbreaks: T list -> T list
val blk: int * T list -> T
val block: T list -> T
val strs: string list -> T
val markup: Markup.T -> T list -> T
val mark: Markup.T -> T -> T
val mark_str: Markup.T * string -> T
val marks_str: Markup.T list * string -> T
val item: T list -> T
val text_fold: T list -> T
val keyword1: string -> T
val keyword2: string -> T
val text: string -> T list
val paragraph: T list -> T
val para: string -> T
val quote: T -> T
val cartouche: T -> T
val separate: string -> T list -> T list
val commas: T list -> T list
val enclose: string -> string -> T list -> T
val enum: string -> string -> string -> T list -> T
val position: Position.T -> T
val here: Position.T -> T list
val list: string -> string -> T list -> T
val str_list: string -> string -> string list -> T
val big_list: string -> T list -> T
val indent: int -> T -> T
val unbreakable: T -> T
val margin_default: int Unsynchronized.ref
val regularN: string
val symbolicN: string
val output_buffer: int option -> T -> Buffer.T
val output: int option -> T -> Output.output
val string_of_margin: int -> T -> string
val string_of: T -> string
val writeln: T -> unit
val symbolic_output: T -> Output.output
val symbolic_string_of: T -> string
val unformatted_string_of: T -> string
val markup_chunks: Markup.T -> T list -> T
val chunks: T list -> T
val chunks2: T list -> T
val block_enclose: T * T -> T list -> T
val writeln_chunks: T list -> unit
val writeln_chunks2: T list -> unit
val to_ML: FixedInt.int -> T -> ML_Pretty.pretty
val from_ML: ML_Pretty.pretty -> T
val to_polyml: T -> PolyML.pretty
val from_polyml: PolyML.pretty -> T
end;
structure Pretty: PRETTY =
struct
(** print mode operations **)
fun default_indent (_: string) = Symbol.spaces;
local
val default = {indent = default_indent};
val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
in
fun add_mode name indent =
Synchronized.change modes (fn tab =>
(if not (Symtab.defined tab name) then ()
else warning ("Redefining pretty mode " ^ quote name);
Symtab.update (name, {indent = indent}) tab));
fun get_mode () =
the_default default
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
end;
fun mode_indent x y = #indent (get_mode ()) x y;
val output_spaces = Output.output o Symbol.spaces;
val add_indent = Buffer.add o output_spaces;
(** printing items: compound phrases, strings, and breaks **)
val force_nat = Integer.max 0;
abstype T =
Block of Markup.output * bool * int * T list * int
(*markup output, consistent, indentation, body, length*)
| Break of bool * int * int (*mandatory flag, width if not taken, extra indentation if taken*)
| Str of Output.output * int (*text, length*)
with
fun length (Block (_, _, _, _, len)) = len
| length (Break (_, wd, _)) = wd
| length (Str (_, len)) = len;
fun make_block {markup, consistent, indent} body =
let
val indent' = force_nat indent;
fun body_length prts len =
let
val (line, rest) = chop_prefix (fn Break (true, _, _) => false | _ => true) prts;
val len' = Int.max (fold (Integer.add o length) line 0, len);
in
(case rest of
Break (true, _, ind) :: rest' =>
body_length (Break (false, indent' + ind, 0) :: rest') len'
| [] => len')
end;
in Block (markup, consistent, indent', body, body_length body 0) end;
fun markup_block {markup, consistent, indent} es =
make_block {markup = Markup.output markup, consistent = consistent, indent = indent} es;
(** derived operations to create formatting expressions **)
val str = Output.output_width ##> force_nat #> Str;
fun brk wd = Break (false, force_nat wd, 0);
fun brk_indent wd ind = Break (false, force_nat wd, ind);
val fbrk = Break (true, 1, 0);
fun breaks prts = Library.separate (brk 1) prts;
fun fbreaks prts = Library.separate fbrk prts;
fun blk (indent, es) =
markup_block {markup = Markup.empty, consistent = false, indent = indent} es;
fun block prts = blk (2, prts);
val strs = block o breaks o map str;
fun markup m = markup_block {markup = m, consistent = false, indent = 0};
fun mark m prt = if m = Markup.empty then prt else markup m [prt];
fun mark_str (m, s) = mark m (str s);
fun marks_str (ms, s) = fold_rev mark ms (str s);
val item = markup Markup.item;
val text_fold = markup Markup.text_fold;
fun keyword1 name = mark_str (Markup.keyword1, name);
fun keyword2 name = mark_str (Markup.keyword2, name);
val text = breaks o map str o Symbol.explode_words;
val paragraph = markup Markup.paragraph;
val para = paragraph o text;
fun quote prt = blk (1, [str "\"", prt, str "\""]);
fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]);
fun separate sep prts =
flat (Library.separate [str sep, brk 1] (map single prts));
val commas = separate ",";
fun enclose lpar rpar prts =
block (str lpar :: (prts @ [str rpar]));
fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
val position =
enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
fun here pos =
let
val props = Position.properties_of pos;
val (s1, s2) = Position.here_strs pos;
in
if s2 = "" then []
else [str s1, mark_str (Markup.properties props Markup.position, s2)]
end;
val list = enum ",";
fun str_list lpar rpar strs = list lpar rpar (map str strs);
fun big_list name prts = block (fbreaks (str name :: prts));
fun indent 0 prt = prt
| indent n prt = blk (0, [str (Symbol.spaces n), prt]);
fun unbreakable (Block (m, consistent, indent, es, len)) =
Block (m, consistent, indent, map unbreakable es, len)
| unbreakable (Break (_, wd, _)) = Str (output_spaces wd, wd)
| unbreakable (e as Str _) = e;
(** formatting **)
(* formatted output *)
local
type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
val empty: text =
{tx = Buffer.empty,
ind = Buffer.empty,
pos = 0,
nl = 0};
fun newline {tx, ind = _, pos = _, nl} : text =
{tx = Buffer.add (Output.output "\n") tx,
ind = Buffer.empty,
pos = 0,
nl = nl + 1};
fun control s {tx, ind, pos: int, nl} : text =
{tx = Buffer.add s tx,
ind = ind,
pos = pos,
nl = nl};
fun string (s, len) {tx, ind, pos: int, nl} : text =
{tx = Buffer.add s tx,
ind = Buffer.add s ind,
pos = pos + len,
nl = nl};
fun blanks wd = string (output_spaces wd, wd);
fun indentation (buf, len) {tx, ind, pos, nl} : text =
let val s = Buffer.content buf in
{tx = Buffer.add (mode_indent s len) tx,
ind = Buffer.add s ind,
pos = pos + len,
nl = nl}
end;
(*Add the lengths of the expressions until the next Break; if no Break then
include "after", to account for text following this block.*)
fun break_dist (Break _ :: _, _) = 0
| break_dist (e :: es, after) = length e + break_dist (es, after)
| break_dist ([], after) = after;
val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
val force_all = map force_break;
(*Search for the next break (at this or higher levels) and force it to occur.*)
fun force_next [] = []
| force_next ((e as Break _) :: es) = force_break e :: es
| force_next (e :: es) = e :: force_next es;
in
fun formatted margin input =
let
val breakgain = margin div 20; (*minimum added space required of a break*)
val emergencypos = margin div 2; (*position too far to right*)
(*es is list of expressions to print;
blockin is the indentation of the current block;
after is the width of the following context until next break.*)
fun format ([], _, _) text = text
| format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
(case e of
Block ((bg, en), consistent, indent, bes, blen) =>
let
val pos' = pos + indent;
val pos'' = pos' mod emergencypos;
val block' =
if pos' < emergencypos then (ind |> add_indent indent, pos')
else (add_indent pos'' Buffer.empty, pos'');
val d = break_dist (es, after)
val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes;
val btext: text = text
|> control bg
|> format (bes', block', d)
|> control en;
(*if this block was broken then force the next break*)
val es' = if nl < #nl btext then force_next es else es;
in format (es', block, after) btext end
| Break (force, wd, ind) =>
(*no break if text to next break fits on this line
or if breaking would add only breakgain to space*)
format (es, block, after)
(if not force andalso
pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain)
then text |> blanks wd (*just insert wd blanks*)
else text |> newline |> indentation block |> blanks ind)
| Str str => format (es, block, after) (string str text));
in
#tx (format ([input], (Buffer.empty, 0), 0) empty)
end;
end;
(* special output *)
(*symbolic markup -- no formatting*)
-fun symbolic prt =
+val symbolic =
let
fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
| out (Block ((bg, en), consistent, indent, prts, _)) =
Buffer.add bg #>
Buffer.markup (Markup.block consistent indent) (fold out prts) #>
Buffer.add en
| out (Break (false, wd, ind)) =
Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
| out (Break (true, _, _)) = Buffer.add (Output.output "\n")
| out (Str (s, _)) = Buffer.add s;
- in out prt Buffer.empty end;
+ in Buffer.build o out end;
(*unformatted output*)
-fun unformatted prt =
+val unformatted =
let
fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
| out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
| out (Str (s, _)) = Buffer.add s;
- in out prt Buffer.empty end;
+ in Buffer.build o out end;
(* output interfaces *)
val margin_default = Unsynchronized.ref ML_Pretty.default_margin; (*right margin, or page width*)
val regularN = "pretty_regular";
val symbolicN = "pretty_symbolic";
fun output_buffer margin prt =
if print_mode_active symbolicN andalso not (print_mode_active regularN)
then symbolic prt
else formatted (the_default (! margin_default) margin) prt;
val output = Buffer.content oo output_buffer;
fun string_of_margin margin = Output.escape o output (SOME margin);
val string_of = Output.escape o output NONE;
val writeln = Output.writeln o string_of;
val symbolic_output = Buffer.content o symbolic;
val symbolic_string_of = Output.escape o symbolic_output;
val unformatted_string_of = Output.escape o Buffer.content o unformatted;
(* chunks *)
fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
val chunks = markup_chunks Markup.empty;
fun chunks2 prts =
(case try split_last prts of
NONE => blk (0, [])
| SOME (prefix, last) =>
blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold;
fun writeln_chunks prts =
Output.writelns (Library.separate "\n" (map string_of_text_fold prts));
fun writeln_chunks2 prts =
(case try split_last prts of
NONE => ()
| SOME (prefix, last) =>
(map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @
[string_of_text_fold last])
|> Output.writelns);
(** toplevel pretty printing **)
fun to_ML 0 (Block _) = ML_Pretty.str "..."
| to_ML depth (Block (m, consistent, indent, prts, _)) =
ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map (to_ML (depth - 1)) prts)
| to_ML _ (Break (force, wd, ind)) =
ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind)
| to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
make_block {markup = m, consistent = consistent, indent = FixedInt.toInt indent}
(map from_ML prts)
| from_ML (ML_Pretty.Break (force, wd, ind)) =
Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
| from_ML (ML_Pretty.String (s, len)) = Str (s, force_nat (FixedInt.toInt len));
val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
val from_polyml = ML_Pretty.from_polyml #> from_ML;
end;
val _ = ML_system_pp (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
val _ = ML_system_pp (fn _ => fn _ => to_polyml o position);
end;
structure ML_Pretty =
struct
open ML_Pretty;
val string_of_polyml = Pretty.string_of o Pretty.from_polyml;
end;
diff --git a/src/Pure/PIDE/xml.ML b/src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML
+++ b/src/Pure/PIDE/xml.ML
@@ -1,422 +1,421 @@
(* Title: Pure/PIDE/xml.ML
Author: David Aspinall
Author: Stefan Berghofer
Author: Makarius
Untyped XML trees and representation of ML values.
*)
signature XML_DATA_OPS =
sig
type 'a A
type 'a T
type 'a V
type 'a P
val int_atom: int A
val bool_atom: bool A
val unit_atom: unit A
val properties: Properties.T T
val string: string T
val int: int T
val bool: bool T
val unit: unit T
val pair: 'a T -> 'b T -> ('a * 'b) T
val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
val list: 'a T -> 'a list T
val option: 'a T -> 'a option T
val variant: 'a V list -> 'a T
end;
signature XML =
sig
type attributes = (string * string) list
datatype tree =
Elem of (string * attributes) * tree list
| Text of string
type body = tree list
val blob: string list -> body
val is_empty: tree -> bool
val is_empty_body: body -> bool
val xml_elemN: string
val xml_nameN: string
val xml_bodyN: string
val wrap_elem: ((string * attributes) * tree list) * tree list -> tree
val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
val add_content: tree -> Buffer.T -> Buffer.T
val content_of: body -> string
val trim_blanks: body -> body
val header: string
val text: string -> string
val element: string -> attributes -> string list -> string
val output_markup: Markup.T -> Markup.output
val string_of: tree -> string
val pretty: int -> tree -> Pretty.T
val parse_comments: string list -> unit * string list
val parse_string : string -> string option
val parse_element: string list -> tree * string list
val parse_document: string list -> tree * string list
val parse: string -> tree
exception XML_ATOM of string
exception XML_BODY of body
structure Encode:
sig
include XML_DATA_OPS
val tree: tree T
end
structure Decode:
sig
include XML_DATA_OPS
val tree: tree T
end
end;
structure XML: XML =
struct
(** XML trees **)
open Output_Primitives.XML;
val blob = map Text;
fun is_empty (Text "") = true
| is_empty _ = false;
val is_empty_body = forall is_empty;
(* wrapped elements *)
val xml_elemN = "xml_elem";
val xml_nameN = "xml_name";
val xml_bodyN = "xml_body";
fun wrap_elem (((a, atts), body1), body2) =
Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', atts'), body1) :: body2)) =
if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN andalso null atts'
then SOME (((a, atts), body1), body2) else NONE
| unwrap_elem _ = NONE;
(* text content *)
fun add_content tree =
(case unwrap_elem tree of
SOME (_, ts) => fold add_content ts
| NONE =>
(case tree of
Elem (_, ts) => fold add_content ts
| Text s => Buffer.add s));
-fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+val content_of = Buffer.build_content o fold add_content;
(* trim blanks *)
fun trim_blanks trees =
trees |> maps
(fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
| Text s =>
let val s' = s |> raw_explode |> trim Symbol.is_blank |> implode;
in if s' = "" then [] else [Text s'] end);
(** string representation **)
val header = "\n";
(* escaped text *)
fun decode "<" = "<"
| decode ">" = ">"
| decode "&" = "&"
| decode "'" = "'"
| decode """ = "\""
| decode c = c;
fun encode "<" = "<"
| encode ">" = ">"
| encode "&" = "&"
| encode "'" = "'"
| encode "\"" = """
| encode c = c;
val text = translate_string encode;
(* elements *)
fun elem name atts =
space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
fun element name atts body =
let val b = implode body in
if b = "" then enclose "<" "/>" (elem name atts)
else enclose "<" ">" (elem name atts) ^ b ^ enclose "" name
end;
fun output_markup (markup as (name, atts)) =
if Markup.is_empty markup then Markup.no_output
else (enclose "<" ">" (elem name atts), enclose "" name);
-(* output *)
+(* output content *)
-fun buffer_of depth tree =
+fun content_depth depth =
let
fun traverse _ (Elem ((name, atts), [])) =
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
| traverse d (Elem ((name, atts), ts)) =
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
traverse_body d ts #>
Buffer.add " Buffer.add name #> Buffer.add ">"
| traverse _ (Text s) = Buffer.add (text s)
and traverse_body 0 _ = Buffer.add "..."
| traverse_body d ts = fold (traverse (d - 1)) ts;
- in Buffer.empty |> traverse depth tree end;
+ in Buffer.build_content o traverse depth end;
-val string_of = Buffer.content o buffer_of ~1;
+val string_of = content_depth ~1;
-fun pretty depth tree =
- Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
+fun pretty depth tree = Pretty.str (content_depth (Int.max (0, depth)) tree);
val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
(** XML parsing **)
local
fun err msg (xs, _) =
fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
fun ignored _ = [];
fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
val parse_name = Scan.one name_start_char ::: Scan.many name_char;
val blanks = Scan.many Symbol.is_blank;
val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode;
val regular = Scan.one Symbol.not_eof;
fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x);
val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
val parse_cdata =
Scan.this_string "") regular) >> implode) --|
Scan.this_string "]]>";
val parse_att =
((parse_name >> implode) --| (blanks -- $$ "=" -- blanks)) --
(($$ "\"" || $$ "'") :|-- (fn s =>
(Scan.repeat (special || regular_except s) >> implode) --| $$ s));
val parse_comment =
Scan.this_string "") regular) --
Scan.this_string "-->" >> ignored;
val parse_processing_instruction =
Scan.this_string "") regular) --
Scan.this_string "?>" >> ignored;
val parse_doctype =
Scan.this_string "") regular) --
$$ ">" >> ignored;
val parse_misc =
Scan.one Symbol.is_blank >> ignored ||
parse_processing_instruction ||
parse_comment;
val parse_optional_text =
Scan.optional (parse_chars >> (single o Text)) [];
in
val parse_comments =
blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
fun parse_content xs =
(parse_optional_text @@@
Scan.repeats
((parse_element >> single ||
parse_cdata >> (single o Text) ||
parse_processing_instruction ||
parse_comment)
@@@ parse_optional_text)) xs
and parse_element xs =
($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
(fn (name, _) =>
!! (err (fn () => "Expected > or />"))
($$ "/" -- $$ ">" >> ignored ||
$$ ">" |-- parse_content --|
!! (err (fn () => "Expected "))
($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
>> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
val parse_document =
(Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
|-- parse_element;
fun parse s =
(case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
(blanks |-- parse_document --| blanks))) (raw_explode s) of
(x, []) => x
| (_, ys) => error ("XML parsing error: unprocessed input\n" ^ Symbol.beginning 100 ys));
end;
(** XML as data representation language **)
exception XML_ATOM of string;
exception XML_BODY of tree list;
structure Encode =
struct
type 'a A = 'a -> string;
type 'a T = 'a -> body;
type 'a V = 'a -> string list * body;
type 'a P = 'a -> string list;
(* atomic values *)
fun int_atom i = Value.print_int i;
fun bool_atom false = "0"
| bool_atom true = "1";
fun unit_atom () = "";
(* structural nodes *)
fun node ts = Elem ((":", []), ts);
fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
(* representation of standard types *)
fun tree (t: tree) = [t];
fun properties props = [Elem ((":", props), [])];
fun string "" = []
| string s = [Text s];
val int = string o int_atom;
val bool = string o bool_atom;
val unit = string o unit_atom;
fun pair f g (x, y) = [node (f x), node (g y)];
fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
fun list f xs = map (node o f) xs;
fun option _ NONE = []
| option f (SOME x) = [node (f x)];
fun variant fs x =
[tagged (the (get_index (fn f => SOME (f x) handle General.Match => NONE) fs))];
end;
structure Decode =
struct
type 'a A = string -> 'a;
type 'a T = body -> 'a;
type 'a V = string list * body -> 'a;
type 'a P = string list -> 'a;
(* atomic values *)
fun int_atom s =
Value.parse_int s
handle Fail _ => raise XML_ATOM s;
fun bool_atom "0" = false
| bool_atom "1" = true
| bool_atom s = raise XML_ATOM s;
fun unit_atom "" = ()
| unit_atom s = raise XML_ATOM s;
(* structural nodes *)
fun node (Elem ((":", []), ts)) = ts
| node t = raise XML_BODY [t];
fun vector atts =
map_index (fn (i, (a, x)) => if int_atom a = i then x else raise XML_ATOM a) atts;
fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
| tagged t = raise XML_BODY [t];
(* representation of standard types *)
fun tree [t] = t
| tree ts = raise XML_BODY ts;
fun properties [Elem ((":", props), [])] = props
| properties ts = raise XML_BODY ts;
fun string [] = ""
| string [Text s] = s
| string ts = raise XML_BODY ts;
val int = int_atom o string;
val bool = bool_atom o string;
val unit = unit_atom o string;
fun pair f g [t1, t2] = (f (node t1), g (node t2))
| pair _ _ ts = raise XML_BODY ts;
fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
| triple _ _ _ ts = raise XML_BODY ts;
fun list f ts = map (f o node) ts;
fun option _ [] = NONE
| option f [t] = SOME (f (node t))
| option _ ts = raise XML_BODY ts;
fun variant fs [t] =
let
val (tag, (xs, ts)) = tagged t;
val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
in f (xs, ts) end
| variant _ ts = raise XML_BODY ts;
end;
end;
diff --git a/src/Pure/PIDE/yxml.ML b/src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML
+++ b/src/Pure/PIDE/yxml.ML
@@ -1,175 +1,175 @@
(* Title: Pure/PIDE/yxml.ML
Author: Makarius
Efficient text representation of XML trees using extra characters X
and Y -- no escaping, may nest marked text verbatim. Suitable for
direct inlining into plain text.
Markup ...body... is encoded as:
X Y name Y att=val ... X
...
body
...
X Y X
*)
signature YXML =
sig
val X: Symbol.symbol
val Y: Symbol.symbol
val embed_controls: string -> string
val detect: string -> bool
val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
val tree_size: XML.tree -> int
val body_size: XML.body -> int
val string_of_body: XML.body -> string
val string_of: XML.tree -> string
val write_body: Path.T -> XML.body -> unit
val output_markup: Markup.T -> string * string
val output_markup_elem: Markup.T -> (string * string) * string
val parse_body: string -> XML.body
val parse: string -> XML.tree
val content_of: string -> string
val is_wellformed: string -> bool
end;
structure YXML: YXML =
struct
(** string representation **)
(* idempotent recoding of certain low ASCII control characters *)
fun pseudo_utf8 c =
if Symbol.is_ascii_control c
then chr 192 ^ chr (128 + ord c)
else c;
fun embed_controls str =
if exists_string Symbol.is_ascii_control str
then translate_string pseudo_utf8 str
else str;
(* markers *)
val X_char = Char.chr 5;
val Y_char = Char.chr 6;
val X = String.str X_char;
val Y = String.str Y_char;
val XY = X ^ Y;
val XYX = XY ^ X;
fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
(* traverse *)
fun traverse string =
let
fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
fun tree (XML.Elem (markup as (name, atts), ts)) =
if Markup.is_empty markup then fold tree ts
else
string XY #> string name #> fold attrib atts #> string X #>
fold tree ts #>
string XYX
| tree (XML.Text s) = string s;
in tree end;
fun tree_size tree = traverse (Integer.add o size) tree 0;
fun body_size body = fold (Integer.add o tree_size) body 0;
(* output *)
-fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
+val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
val string_of = string_of_body o single;
fun write_body path body =
path |> File.open_output (fn file =>
fold (traverse (fn s => fn () => File.output file s)) body ());
(* markup elements *)
val Z = chr 0;
val Z_text = [XML.Text Z];
fun output_markup (markup as (name, atts)) =
if Markup.is_empty markup then Markup.no_output
else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
fun output_markup_elem markup =
let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
in ((bg1, bg2), en) end;
(** efficient YXML parsing **)
local
(* splitting *)
val split_string =
Substring.full #>
Substring.tokens (fn c => c = X_char) #>
map (Substring.fields (fn c => c = Y_char) #> map Substring.string);
(* structural errors *)
fun err msg = raise Fail ("Malformed YXML: " ^ msg);
fun err_attribute () = err "bad attribute";
fun err_element () = err "bad element";
fun err_unbalanced "" = err "unbalanced element"
| err_unbalanced name = err ("unbalanced element " ^ quote name);
(* stack operations *)
fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
fun push "" _ _ = err_element ()
| push name atts pending = ((name, atts), []) :: pending;
fun pop ((("", _), _) :: _) = err_unbalanced ""
| pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
(* parsing *)
fun parse_attrib s =
(case first_field "=" s of
NONE => err_attribute ()
| SOME ("", _) => err_attribute ()
| SOME att => att);
fun parse_chunk ["", ""] = pop
| parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
| parse_chunk txts = fold (add o XML.Text) txts;
in
fun parse_body source =
(case fold parse_chunk (split_string source) [(("", []), [])] of
[(("", _), result)] => rev result
| ((name, _), _) :: _ => err_unbalanced name);
fun parse source =
(case parse_body source of
[result] => result
| [] => XML.Text ""
| _ => err "multiple results");
end;
val content_of = parse_body #> XML.content_of;
fun is_wellformed s = string_of_body (parse_body s) = s
handle Fail _ => false;
end;
diff --git a/src/Tools/Code/code_printer.ML b/src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML
+++ b/src/Tools/Code/code_printer.ML
@@ -1,449 +1,448 @@
(* Title: Tools/Code/code_printer.ML
Author: Florian Haftmann, TU Muenchen
Generic operations for pretty printing of target language code.
*)
signature CODE_PRINTER =
sig
type itype = Code_Thingol.itype
type iterm = Code_Thingol.iterm
type const = Code_Thingol.const
type dict = Code_Thingol.dict
val eqn_error: theory -> thm option -> string -> 'a
val @@ : 'a * 'a -> 'a list
val @| : 'a list * 'a -> 'a list
val str: string -> Pretty.T
val concat: Pretty.T list -> Pretty.T
val brackets: Pretty.T list -> Pretty.T
val enclose: string -> string -> Pretty.T list -> Pretty.T
val commas: Pretty.T list -> Pretty.T list
val enum: string -> string -> string -> Pretty.T list -> Pretty.T
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
val semicolon: Pretty.T list -> Pretty.T
val doublesemicolon: Pretty.T list -> Pretty.T
val indent: int -> Pretty.T -> Pretty.T
val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
val format: Code_Symbol.T list -> int -> Pretty.T -> string
type var_ctxt
val make_vars: string list -> var_ctxt
val intro_vars: string list -> var_ctxt -> var_ctxt
val lookup_var: var_ctxt -> string -> string
val intro_base_names: (string -> bool) -> (string -> string)
-> string list -> var_ctxt -> var_ctxt
val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string)
-> iterm list -> var_ctxt -> var_ctxt
val aux_params: var_ctxt -> iterm list list -> string list
type literals
val Literals: { literal_string: string -> string,
literal_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
-> literals
val literal_string: literals -> string -> string
val literal_numeral: literals -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
val infix_cons: literals -> int * string
type lrx
val L: lrx
val R: lrx
val X: lrx
type fixity
val BR: fixity
val NOBR: fixity
val INFX: int * lrx -> fixity
val APP: fixity
val brackify: fixity -> Pretty.T list -> Pretty.T
val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
type raw_const_syntax
val plain_const_syntax: string -> raw_const_syntax
type simple_const_syntax
val simple_const_syntax: simple_const_syntax -> raw_const_syntax
type complex_const_syntax
val complex_const_syntax: complex_const_syntax -> raw_const_syntax
val parse_const_syntax: raw_const_syntax parser
val requires_args: raw_const_syntax -> int
datatype const_printer = Plain_printer of string
| Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T
type const_syntax = int * const_printer
val prep_const_syntax: theory -> literals
-> string -> raw_const_syntax -> const_syntax
type tyco_syntax
val parse_tyco_syntax: tyco_syntax parser
val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
-> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> const_syntax option)
-> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> fixity
-> iterm -> var_ctxt -> Pretty.T * var_ctxt
type identifiers
type printings
type data
val empty_data: data
val map_data: (string list * identifiers * printings
-> string list * identifiers * printings)
-> data -> data
val merge_data: data * data -> data
val the_reserved: data -> string list;
val the_identifiers: data -> identifiers;
val the_printings: data -> printings;
end;
structure Code_Printer : CODE_PRINTER =
struct
open Basic_Code_Symbol;
open Code_Thingol;
(** generic nonsense *)
fun eqn_error thy (SOME thm) s =
error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm)
| eqn_error _ NONE s = error s;
val code_presentationN = "code_presentation";
val stmt_nameN = "stmt_name";
val _ = Markup.add_mode code_presentationN YXML.output_markup;
(** assembling and printing text pieces **)
infixr 5 @@;
infixr 5 @|;
fun x @@ y = [x, y];
fun xs @| y = xs @ [y];
fun with_no_print_mode f = Print_Mode.setmp [] f;
val str = with_no_print_mode Pretty.str;
val concat = Pretty.block o Pretty.breaks;
val commas = with_no_print_mode Pretty.commas;
fun enclose l r = with_no_print_mode (Pretty.enclose l r);
val brackets = enclose "(" ")" o Pretty.breaks;
fun enum sep l r = with_no_print_mode (Pretty.enum sep l r);
fun enum_default default sep l r [] = str default
| enum_default default sep l r xs = enum sep l r xs;
fun semicolon ps = Pretty.block [concat ps, str ";"];
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
fun indent i = with_no_print_mode (Pretty.indent i);
fun with_presentation_marker f = Print_Mode.setmp [code_presentationN] f;
fun markup_stmt sym = with_presentation_marker
(Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
-fun filter_presentation [] tree =
- Buffer.empty
- |> fold XML.add_content tree
- | filter_presentation presentation_syms tree =
+fun filter_presentation [] xml =
+ Buffer.build (fold XML.add_content xml)
+ | filter_presentation presentation_syms xml =
let
val presentation_idents = map Code_Symbol.marker presentation_syms
fun is_selected (name, attrs) =
name = code_presentationN
andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
fun add_content_with_space tree (is_first, buf) =
buf
|> not is_first ? Buffer.add "\n\n"
|> XML.add_content tree
|> pair false;
fun filter (XML.Elem (name_attrs, xs)) =
fold (if is_selected name_attrs then add_content_with_space else filter) xs
| filter (XML.Text _) = I;
- in snd (fold filter tree (true, Buffer.empty)) end;
+ in snd (fold filter xml (true, Buffer.empty)) end;
fun format presentation_names width =
with_presentation_marker (Pretty.string_of_margin width)
#> YXML.parse_body
#> filter_presentation presentation_names
#> Buffer.add "\n"
#> Buffer.content;
(** names and variable name contexts **)
type var_ctxt = string Symtab.table * Name.context;
fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
Name.make_context names);
fun intro_vars names (namemap, namectxt) =
let
val (names', namectxt') = fold_map Name.variant names namectxt;
val namemap' = fold2 (curry Symtab.update) names names' namemap;
in (namemap', namectxt') end;
fun lookup_var (namemap, _) name =
case Symtab.lookup namemap name of
SOME name' => name'
| NONE => error ("Invalid name in context: " ^ quote name);
fun aux_params vars lhss =
let
fun fish_param _ (w as SOME _) = w
| fish_param (IVar (SOME v)) NONE = SOME v
| fish_param _ NONE = NONE;
fun fillup_param _ (_, SOME v) = v
| fillup_param x (i, NONE) = x ^ string_of_int i;
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
val x = singleton (Name.variant_list (map_filter I fished1)) "x";
val fished2 = map_index (fillup_param x) fished1;
val (fished3, _) = fold_map Name.variant fished2 Name.context;
val vars' = intro_vars fished3 vars;
in map (lookup_var vars') fished3 end;
fun intro_base_names no_syntax deresolve =
map_filter (fn name => if no_syntax name then
let val name' = deresolve name in
if Long_Name.is_qualified name' then NONE else SOME name'
end else NONE)
#> intro_vars;
fun intro_base_names_for no_syntax deresolve ts =
[]
|> fold Code_Thingol.add_constsyms ts
|> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve;
(** pretty literals **)
datatype literals = Literals of {
literal_string: string -> string,
literal_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T,
infix_cons: int * string
};
fun dest_Literals (Literals lits) = lits;
val literal_string = #literal_string o dest_Literals;
val literal_numeral = #literal_numeral o dest_Literals;
val literal_list = #literal_list o dest_Literals;
val infix_cons = #infix_cons o dest_Literals;
(** syntax printer **)
(* binding priorities *)
datatype lrx = L | R | X;
datatype fixity =
BR
| NOBR
| INFX of (int * lrx);
val APP = INFX (~1, L);
fun fixity_lrx L L = false
| fixity_lrx R R = false
| fixity_lrx _ _ = true;
fun fixity NOBR _ = false
| fixity _ NOBR = false
| fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
pr < pr_ctxt
orelse pr = pr_ctxt
andalso fixity_lrx lr lr_ctxt
orelse pr_ctxt = ~1
| fixity BR (INFX _) = false
| fixity _ _ = true;
fun gen_brackify _ [p] = p
| gen_brackify true (ps as _::_) = enclose "(" ")" ps
| gen_brackify false (ps as _::_) = Pretty.block ps;
fun brackify fxy_ctxt =
gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
fun brackify_infix infx fxy_ctxt (l, m, r) =
gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r];
fun brackify_block fxy_ctxt p1 ps p2 =
let val p = Pretty.block_enclose (p1, p2) ps
in if fixity BR fxy_ctxt
then enclose "(" ")" [p]
else p
end;
fun gen_applify strict opn cls f fxy_ctxt p [] =
if strict
then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)]
else p
| gen_applify strict opn cls f fxy_ctxt p ps =
gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps));
fun applify opn = gen_applify false opn;
fun tuplify _ _ [] = NONE
| tuplify print fxy [x] = SOME (print fxy x)
| tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
(* generic syntax *)
type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T);
type complex_const_syntax = int * (literals
-> (var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
datatype raw_const_syntax = plain_const_syntax of string
| complex_const_syntax of complex_const_syntax;
fun simple_const_syntax syn =
complex_const_syntax
(apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn);
fun requires_args (plain_const_syntax _) = 0
| requires_args (complex_const_syntax (k, _)) = k;
datatype const_printer = Plain_printer of string
| Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T;
type const_syntax = int * const_printer;
fun prep_const_syntax thy literals c (plain_const_syntax s) =
(Code.args_number thy c, Plain_printer s)
| prep_const_syntax thy literals c (complex_const_syntax (n, f))=
(n, Complex_printer (f literals));
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
(app as ({ sym, dom, ... }, ts)) =
case sym of
Constant const => (case const_syntax const of
NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (_, Plain_printer s) =>
brackify fxy (str s :: map (print_term some_thm vars BR) ts)
| SOME (k, Complex_printer print) =>
let
fun print' fxy ts =
print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
in
if k = length ts
then print' fxy ts
else if k < length ts
then case chop k ts of (ts1, ts2) =>
brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
end)
| _ => brackify fxy (print_app_expr some_thm vars app);
fun gen_print_bind print_term thm (fxy : fixity) pat vars =
let
val vs = Code_Thingol.fold_varnames (insert (op =)) pat [];
val vars' = intro_vars vs vars;
in (print_term thm vars' fxy pat, vars') end;
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
-> fixity -> itype list -> Pretty.T);
(* mixfix syntax *)
datatype 'a mixfix =
Arg of fixity
| String of string
| Break;
fun printer_of_mixfix prep_arg (fixity_this, mfx) =
let
fun is_arg (Arg _) = true
| is_arg _ = false;
val i = (length o filter is_arg) mfx;
fun fillin _ [] [] =
[]
| fillin print (Arg fxy :: mfx) (a :: args) =
(print fxy o prep_arg) a :: fillin print mfx args
| fillin print (String s :: mfx) args =
str s :: fillin print mfx args
| fillin print (Break :: mfx) args =
Pretty.brk 1 :: fillin print mfx args;
in
(i, fn print => fn fixity_ctxt => fn args =>
gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
end;
fun read_infix (fixity_this, i) s =
let
val l = case fixity_this of L => INFX (i, L) | _ => INFX (i, X);
val r = case fixity_this of R => INFX (i, R) | _ => INFX (i, X);
in
(INFX (i, fixity_this), [Arg l, String " ", String s, Break, Arg r])
end;
fun read_mixfix s =
let
val sym_any = Scan.one Symbol.not_eof;
val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat (
($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
|| ($$ "_" >> K (Arg BR))
|| ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break))
|| (Scan.repeat1
( $$ "'" |-- sym_any
|| Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
sym_any) >> (String o implode)));
fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s)
| err _ (_, SOME msg) = msg;
in
case Scan.finite Symbol.stopper parse (Symbol.explode s) of
(fixity_mixfix, []) => fixity_mixfix
| _ => Scan.!! (err s) Scan.fail ()
end;
val parse_fixity =
(\<^keyword>\infix\ >> K X) || (\<^keyword>\infixl\ >> K L) || (\<^keyword>\infixr\ >> K R)
fun parse_mixfix x =
(Parse.string >> read_mixfix
|| parse_fixity -- Parse.nat -- Parse.string
>> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x;
fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s
| syntax_of_mixfix of_plain of_printer prep_arg (fixity, mfx) =
of_printer (printer_of_mixfix prep_arg (fixity, mfx));
fun parse_tyco_syntax x =
(parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x;
val parse_const_syntax =
parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst;
(** custom data structure **)
type identifiers = (string list * string, string list * string, string list * string, string list * string,
string list * string, string list * string) Code_Symbol.data;
type printings = (const_syntax, tyco_syntax, string, unit, unit,
(Pretty.T * Code_Symbol.T list)) Code_Symbol.data;
datatype data = Data of { reserved: string list, identifiers: identifiers,
printings: printings };
fun make_data (reserved, identifiers, printings) =
Data { reserved = reserved, identifiers = identifiers, printings = printings };
val empty_data = make_data ([], Code_Symbol.empty_data, Code_Symbol.empty_data);
fun map_data f (Data { reserved, identifiers, printings }) =
make_data (f (reserved, identifiers, printings));
fun merge_data (Data { reserved = reserved1, identifiers = identifiers1, printings = printings1 },
Data { reserved = reserved2, identifiers = identifiers2, printings = printings2 }) =
make_data (merge (op =) (reserved1, reserved2),
Code_Symbol.merge_data (identifiers1, identifiers2), Code_Symbol.merge_data (printings1, printings2));
fun the_reserved (Data { reserved, ... }) = reserved;
fun the_identifiers (Data { identifiers , ... }) = identifiers;
fun the_printings (Data { printings, ... }) = printings;
end; (*struct*)
diff --git a/src/Tools/Haskell/Haskell.thy b/src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy
+++ b/src/Tools/Haskell/Haskell.thy
@@ -1,3811 +1,3818 @@
(* Title: Tools/Haskell/Haskell.thy
Author: Makarius
Support for Isabelle tools in Haskell.
*)
theory Haskell
imports Main
begin
generate_file "Isabelle/Bytes.hs" = \
{- Title: Isabelle/Bytes.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Compact byte strings.
See \<^file>\$ISABELLE_HOME/src/Pure/General/bytes.ML\
and \<^file>\$ISABELLE_HOME/src/Pure/General/bytes.scala\.
-}
{-# LANGUAGE TypeApplications #-}
module Isabelle.Bytes (
Bytes,
make, unmake, pack, unpack,
empty, null, length, index, all, any,
head, last, take, drop, isPrefixOf, isSuffixOf, try_unprefix, try_unsuffix,
concat, space, spaces, char, all_char, any_char, byte, singleton
)
where
import Prelude hiding (null, length, all, any, head, last, take, drop, concat)
import qualified Data.ByteString.Short as ShortByteString
import Data.ByteString.Short (ShortByteString)
import qualified Data.ByteString as ByteString
import Data.ByteString (ByteString)
import qualified Data.List as List
import Data.Word (Word8)
import Data.Array (Array, array, (!))
type Bytes = ShortByteString
make :: ByteString -> Bytes
make = ShortByteString.toShort
unmake :: Bytes -> ByteString
unmake = ShortByteString.fromShort
pack :: [Word8] -> Bytes
pack = ShortByteString.pack
unpack :: Bytes -> [Word8]
unpack = ShortByteString.unpack
empty :: Bytes
empty = ShortByteString.empty
null :: Bytes -> Bool
null = ShortByteString.null
length :: Bytes -> Int
length = ShortByteString.length
index :: Bytes -> Int -> Word8
index = ShortByteString.index
all :: (Word8 -> Bool) -> Bytes -> Bool
all p = List.all p . unpack
any :: (Word8 -> Bool) -> Bytes -> Bool
any p = List.any p . unpack
head :: Bytes -> Word8
head bytes = index bytes 0
last :: Bytes -> Word8
last bytes = index bytes (length bytes - 1)
take :: Int -> Bytes -> Bytes
take n bs
| n == 0 = empty
| n >= length bs = bs
| otherwise = pack (List.take n (unpack bs))
drop :: Int -> Bytes -> Bytes
drop n bs
| n == 0 = bs
| n >= length bs = empty
| otherwise = pack (List.drop n (unpack bs))
isPrefixOf :: Bytes -> Bytes -> Bool
isPrefixOf bs1 bs2 =
n1 <= n2 && List.all (\i -> index bs1 i == index bs2 i) [0 .. n1 - 1]
where n1 = length bs1; n2 = length bs2
isSuffixOf :: Bytes -> Bytes -> Bool
isSuffixOf bs1 bs2 =
n1 <= n2 && List.all (\i -> index bs1 i == index bs2 (i + k)) [0 .. n1 - 1]
where n1 = length bs1; n2 = length bs2; k = n2 - n1
try_unprefix :: Bytes -> Bytes -> Maybe Bytes
try_unprefix bs1 bs2 =
if isPrefixOf bs1 bs2 then Just (drop (length bs1) bs2)
else Nothing
try_unsuffix :: Bytes -> Bytes -> Maybe Bytes
try_unsuffix bs1 bs2 =
if isSuffixOf bs1 bs2 then Just (take (length bs2 - length bs1) bs2)
else Nothing
concat :: [Bytes] -> Bytes
concat = mconcat
space :: Word8
space = 32
small_spaces :: Array Int Bytes
small_spaces = array (0, 64) [(i, pack (replicate i space)) | i <- [0 .. 64]]
spaces :: Int -> Bytes
spaces n =
if n < 64 then small_spaces ! n
else concat ((small_spaces ! (n `mod` 64)) : replicate (n `div` 64) (small_spaces ! 64))
char :: Word8 -> Char
char = toEnum . fromEnum
all_char :: (Char -> Bool) -> Bytes -> Bool
all_char pred = all (pred . char)
any_char :: (Char -> Bool) -> Bytes -> Bool
any_char pred = any (pred . char)
byte :: Char -> Word8
byte = toEnum . fromEnum
singletons :: Array Word8 Bytes
singletons =
array (minBound, maxBound)
[(i, make (ByteString.singleton i)) | i <- [minBound .. maxBound]]
singleton :: Word8 -> Bytes
singleton b = singletons ! b
\
generate_file "Isabelle/UTF8.hs" = \
{- Title: Isabelle/UTF8.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Variations on UTF-8.
See \<^file>\$ISABELLE_HOME/src/Pure/General/utf8.ML\
and \<^file>\$ISABELLE_HOME/src/Pure/General/utf8.scala\.
-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
module Isabelle.UTF8 (
setup, setup3,
Recode (..)
)
where
import qualified System.IO as IO
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Text.Encoding as Encoding
import qualified Data.Text.Encoding.Error as Error
import Data.ByteString (ByteString)
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
setup :: IO.Handle -> IO ()
setup h = do
IO.hSetEncoding h IO.utf8
IO.hSetNewlineMode h IO.noNewlineTranslation
setup3 :: IO.Handle -> IO.Handle -> IO.Handle -> IO ()
setup3 h1 h2 h3 = do
setup h1
setup h2
setup h3
class Recode a b where
encode :: a -> b
decode :: b -> a
instance Recode Text ByteString where
encode :: Text -> ByteString
encode = Encoding.encodeUtf8
decode :: ByteString -> Text
decode = Encoding.decodeUtf8With Error.lenientDecode
instance Recode Text Bytes where
encode :: Text -> Bytes
encode = Bytes.make . encode
decode :: Bytes -> Text
decode = decode . Bytes.unmake
instance Recode String ByteString where
encode :: String -> ByteString
encode = encode . Text.pack
decode :: ByteString -> String
decode = Text.unpack . decode
instance Recode String Bytes where
encode :: String -> Bytes
encode = encode . Text.pack
decode :: Bytes -> String
decode = Text.unpack . decode
\
generate_file "Isabelle/Library.hs" = \
{- Title: Isabelle/Library.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Basic library of Isabelle idioms.
See \<^file>\$ISABELLE_HOME/src/Pure/General/basics.ML\
and \<^file>\$ISABELLE_HOME/src/Pure/library.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
module Isabelle.Library (
(|>), (|->), (#>), (#->),
fold, fold_rev, single, the_single, singletonM, map_index, get_index, separate,
StringLike, STRING (..), TEXT (..), BYTES (..),
show_bytes, show_text,
proper_string, enclose, quote, space_implode, commas, commas_quote, cat_lines,
space_explode, split_lines, trim_line, trim_split_lines,
getenv, getenv_strict)
where
import System.Environment (lookupEnv)
import Data.Maybe (fromMaybe)
import qualified Data.Text as Text
import Data.Text (Text)
import qualified Data.Text.Lazy as Lazy
import Data.String (IsString)
import qualified Data.List.Split as Split
import qualified Isabelle.Symbol as Symbol
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
import qualified Isabelle.UTF8 as UTF8
{- functions -}
(|>) :: a -> (a -> b) -> b
x |> f = f x
(|->) :: (a, b) -> (a -> b -> c) -> c
(x, y) |-> f = f x y
(#>) :: (a -> b) -> (b -> c) -> a -> c
(f #> g) x = x |> f |> g
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
(f #-> g) x = x |> f |-> g
{- lists -}
fold :: (a -> b -> b) -> [a] -> b -> b
fold _ [] y = y
fold f (x : xs) y = fold f xs (f x y)
fold_rev :: (a -> b -> b) -> [a] -> b -> b
fold_rev _ [] y = y
fold_rev f (x : xs) y = f x (fold_rev f xs y)
single :: a -> [a]
single x = [x]
the_single :: [a] -> a
the_single [x] = x
the_single _ = undefined
singletonM :: Monad m => ([a] -> m [b]) -> a -> m b
singletonM f x = the_single <$> f [x]
map_index :: ((Int, a) -> b) -> [a] -> [b]
map_index f = map_aux 0
where
map_aux _ [] = []
map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
get_index f = get_aux 0
where
get_aux _ [] = Nothing
get_aux i (x : xs) =
case f x of
Nothing -> get_aux (i + 1) xs
Just y -> Just (i, y)
separate :: a -> [a] -> [a]
separate s (x : (xs @ (_ : _))) = x : s : separate s xs
separate _ xs = xs;
{- string-like interfaces -}
class (IsString a, Monoid a, Eq a, Ord a) => StringLike a where
space_explode :: Char -> a -> [a]
trim_line :: a -> a
gen_trim_line :: Int -> (Int -> Char) -> (Int -> a -> a) -> a -> a
gen_trim_line n at trim s =
if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then trim (n - 2) s
else if n >= 1 && Symbol.is_ascii_line_terminator (at (n - 1)) then trim (n - 1) s
else s
instance StringLike String where
space_explode :: Char -> String -> [String]
space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
trim_line :: String -> String
trim_line s = gen_trim_line (length s) ((!!) s) take s
instance StringLike Text where
space_explode :: Char -> Text -> [Text]
space_explode c str =
if Text.null str then []
else if Text.all (/= c) str then [str]
else map Text.pack $ space_explode c $ Text.unpack str
trim_line :: Text -> Text
trim_line s = gen_trim_line (Text.length s) (Text.index s) Text.take s
instance StringLike Lazy.Text where
space_explode :: Char -> Lazy.Text -> [Lazy.Text]
space_explode c str =
if Lazy.null str then []
else if Lazy.all (/= c) str then [str]
else map Lazy.pack $ space_explode c $ Lazy.unpack str
trim_line :: Lazy.Text -> Lazy.Text
trim_line = Lazy.fromStrict . trim_line . Lazy.toStrict
instance StringLike Bytes where
space_explode :: Char -> Bytes -> [Bytes]
space_explode c str =
if Bytes.null str then []
else if Bytes.all_char (/= c) str then [str]
else
explode (Bytes.unpack str)
where
explode rest =
case span (/= (Bytes.byte c)) rest of
(_, []) -> [Bytes.pack rest]
(prfx, _ : rest') -> Bytes.pack prfx : explode rest'
trim_line :: Bytes -> Bytes
trim_line s = gen_trim_line (Bytes.length s) (Bytes.char . Bytes.index s) Bytes.take s
class StringLike a => STRING a where make_string :: a -> String
instance STRING String where make_string = id
instance STRING Text where make_string = Text.unpack
instance STRING Lazy.Text where make_string = Lazy.unpack
instance STRING Bytes where make_string = UTF8.decode
class StringLike a => TEXT a where make_text :: a -> Text
instance TEXT String where make_text = Text.pack
instance TEXT Text where make_text = id
instance TEXT Lazy.Text where make_text = Lazy.toStrict
instance TEXT Bytes where make_text = UTF8.decode
class StringLike a => BYTES a where make_bytes :: a -> Bytes
instance BYTES String where make_bytes = UTF8.encode
instance BYTES Text where make_bytes = UTF8.encode
instance BYTES Lazy.Text where make_bytes = UTF8.encode . Lazy.toStrict
instance BYTES Bytes where make_bytes = id
show_bytes :: Show a => a -> Bytes
show_bytes = make_bytes . show
show_text :: Show a => a -> Text
show_text = make_text . show
{- strings -}
proper_string :: StringLike a => a -> Maybe a
proper_string s = if s == "" then Nothing else Just s
enclose :: StringLike a => a -> a -> a -> a
enclose lpar rpar str = lpar <> str <> rpar
quote :: StringLike a => a -> a
quote = enclose "\"" "\""
space_implode :: StringLike a => a -> [a] -> a
space_implode s = mconcat . separate s
commas, commas_quote :: StringLike a => [a] -> a
commas = space_implode ", "
commas_quote = commas . map quote
split_lines :: StringLike a => a -> [a]
split_lines = space_explode '\n'
cat_lines :: StringLike a => [a] -> a
cat_lines = space_implode "\n"
trim_split_lines :: StringLike a => a -> [a]
trim_split_lines = trim_line #> split_lines #> map trim_line
{- getenv -}
getenv :: Bytes -> IO Bytes
getenv x = do
y <- lookupEnv (make_string x)
return $ make_bytes $ fromMaybe "" y
getenv_strict :: Bytes -> IO Bytes
getenv_strict x = do
y <- getenv x
if Bytes.null y then
errorWithoutStackTrace $ make_string ("Undefined Isabelle environment variable: " <> quote x)
else return y
\
generate_file "Isabelle/Symbol.hs" = \
{- Title: Isabelle/Symbols.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Isabelle text symbols.
See \<^file>\$ISABELLE_HOME/src/Pure/General/symbol.ML\
and \<^file>\$ISABELLE_HOME/src/Pure/General/symbol_explode.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
module Isabelle.Symbol (
Symbol, eof, is_eof, not_eof,
is_ascii_letter, is_ascii_digit, is_ascii_hex, is_ascii_quasi,
is_ascii_blank, is_ascii_line_terminator, is_ascii_letdig,
is_ascii_identifier,
explode
)
where
import Data.Word (Word8)
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
{- type -}
type Symbol = Bytes
eof :: Symbol
eof = ""
is_eof, not_eof :: Symbol -> Bool
is_eof = Bytes.null
not_eof = not . is_eof
{- ASCII characters -}
is_ascii_letter :: Char -> Bool
is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
is_ascii_digit :: Char -> Bool
is_ascii_digit c = '0' <= c && c <= '9'
is_ascii_hex :: Char -> Bool
is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'
is_ascii_quasi :: Char -> Bool
is_ascii_quasi c = c == '_' || c == '\''
is_ascii_blank :: Char -> Bool
is_ascii_blank c = c `elem` (" \t\n\11\f\r" :: String)
is_ascii_line_terminator :: Char -> Bool
is_ascii_line_terminator c = c == '\r' || c == '\n'
is_ascii_letdig :: Char -> Bool
is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c
is_ascii_identifier :: String -> Bool
is_ascii_identifier s =
not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s
{- explode symbols: ASCII, UTF8, named -}
is_utf8 :: Word8 -> Bool
is_utf8 b = b >= 128
is_utf8_trailer :: Word8 -> Bool
is_utf8_trailer b = 128 <= b && b < 192
is_utf8_control :: Word8 -> Bool
is_utf8_control b = 128 <= b && b < 160
(|>) :: a -> (a -> b) -> b
x |> f = f x
explode :: Bytes -> [Symbol]
explode string = scan 0
where
byte = Bytes.index string
substring i j =
if i == j - 1 then Bytes.singleton (byte i)
else Bytes.pack (map byte [i .. j - 1])
n = Bytes.length string
test pred i = i < n && pred (byte i)
test_char pred i = i < n && pred (Bytes.char (byte i))
many pred i = if test pred i then many pred (i + 1) else i
maybe_char c i = if test_char (== c) i then i + 1 else i
maybe_ascii_id i =
if test_char is_ascii_letter i
then many (is_ascii_letdig . Bytes.char) (i + 1)
else i
scan i =
if i < n then
let
b = byte i
c = Bytes.char b
in
{-encoded newline-}
if c == '\r' then "\n" : scan (maybe_char '\n' (i + 1))
{-pseudo utf8: encoded ascii control-}
else if b == 192 && test is_utf8_control (i + 1) && not (test is_utf8 (i + 2))
then Bytes.singleton (byte (i + 1) - 128) : scan (i + 2)
{-utf8-}
else if is_utf8 b then
let j = many is_utf8_trailer (i + 1)
in substring i j : scan j
{-named symbol-}
else if c == '\\' && test_char (== '<') (i + 1) then
let j = (i + 2) |> maybe_char '^' |> maybe_ascii_id |> maybe_char '>'
in substring i j : scan j
{-single character-}
else Bytes.singleton b : scan (i + 1)
else []
\
generate_file "Isabelle/Buffer.hs" = \
{- Title: Isabelle/Buffer.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Efficient buffer of byte strings.
See \<^file>\$ISABELLE_HOME/src/Pure/General/buffer.ML\.
-}
-module Isabelle.Buffer (T, empty, add, content)
+module Isabelle.Buffer (T, empty, add, content, build, build_content)
where
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
+import Isabelle.Library
newtype T = Buffer [Bytes]
empty :: T
empty = Buffer []
add :: Bytes -> T -> T
add b (Buffer bs) = Buffer (if Bytes.null b then bs else b : bs)
content :: T -> Bytes
content (Buffer bs) = Bytes.concat (reverse bs)
+
+build :: (T -> T) -> T
+build f = f empty
+
+build_content :: (T -> T) -> Bytes
+build_content f = build f |> content
\
generate_file "Isabelle/Value.hs" = \
{- Title: Isabelle/Value.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Plain values, represented as string.
See \<^file>\$ISABELLE_HOME/src/Pure/General/value.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
module Isabelle.Value
(print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real)
where
import qualified Data.List as List
import qualified Text.Read as Read
import Isabelle.Bytes (Bytes)
import Isabelle.Library
{- bool -}
print_bool :: Bool -> Bytes
print_bool True = "true"
print_bool False = "false"
parse_bool :: Bytes -> Maybe Bool
parse_bool "true" = Just True
parse_bool "false" = Just False
parse_bool _ = Nothing
{- nat -}
parse_nat :: Bytes -> Maybe Int
parse_nat s =
case Read.readMaybe (make_string s) of
Just n | n >= 0 -> Just n
_ -> Nothing
{- int -}
print_int :: Int -> Bytes
print_int = show_bytes
parse_int :: Bytes -> Maybe Int
parse_int = Read.readMaybe . make_string
{- real -}
print_real :: Double -> Bytes
print_real x =
let s = show x in
case span (/= '.') s of
(a, '.' : b) | List.all (== '0') b -> make_bytes a
_ -> make_bytes s
parse_real :: Bytes -> Maybe Double
parse_real = Read.readMaybe . make_string
\
generate_file "Isabelle/Properties.hs" = \
{- Title: Isabelle/Properties.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Property lists.
See \<^file>\$ISABELLE_HOME/src/Pure/General/properties.ML\.
-}
module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
where
import qualified Data.List as List
import Isabelle.Bytes (Bytes)
type Entry = (Bytes, Bytes)
type T = [Entry]
defined :: T -> Bytes -> Bool
defined props name = any (\(a, _) -> a == name) props
get :: T -> Bytes -> Maybe Bytes
get props name = List.lookup name props
get_value :: (Bytes -> Maybe a) -> T -> Bytes -> Maybe a
get_value parse props name =
case get props name of
Nothing -> Nothing
Just s -> parse s
put :: Entry -> T -> T
put entry props = entry : remove (fst entry) props
remove :: Bytes -> T -> T
remove name props =
if defined props name then filter (\(a, _) -> a /= name) props
else props
\
generate_file "Isabelle/Markup.hs" = \
{- Title: Isabelle/Markup.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Quasi-abstract markup elements.
See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/markup.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Isabelle.Markup (
T, empty, is_empty, properties,
nameN, name, xnameN, xname, kindN,
bindingN, binding, entityN, entity, defN, refN,
completionN, completion, no_completionN, no_completion,
lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
position_properties, def_name,
expressionN, expression,
citationN, citation,
pathN, path, urlN, url, docN, doc,
markupN, consistentN, unbreakableN, indentN, widthN,
blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
wordsN, words,
tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
inner_cartoucheN, inner_cartouche,
token_rangeN, token_range,
sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
antiquotedN, antiquoted, antiquoteN, antiquote,
paragraphN, paragraph, text_foldN, text_fold,
keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
comment2N, comment2, comment3N, comment3,
forkedN, forked, joinedN, joined, runningN, running, finishedN, finished,
failedN, failed, canceledN, canceled, initializedN, initialized, finalizedN, finalized,
consolidatedN, consolidated,
writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
intensifyN, intensify,
Output, no_output)
where
import Prelude hiding (words, error, break)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Isabelle.Library
import qualified Isabelle.Properties as Properties
import qualified Isabelle.Value as Value
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
{- basic markup -}
type T = (Bytes, Properties.T)
empty :: T
empty = ("", [])
is_empty :: T -> Bool
is_empty ("", _) = True
is_empty _ = False
properties :: Properties.T -> T -> T
properties more_props (elem, props) =
(elem, fold_rev Properties.put more_props props)
markup_elem :: Bytes -> T
markup_elem name = (name, [])
markup_string :: Bytes -> Bytes -> Bytes -> T
markup_string name prop = \s -> (name, [(prop, s)])
{- misc properties -}
nameN :: Bytes
nameN = \Markup.nameN\
name :: Bytes -> T -> T
name a = properties [(nameN, a)]
xnameN :: Bytes
xnameN = \Markup.xnameN\
xname :: Bytes -> T -> T
xname a = properties [(xnameN, a)]
kindN :: Bytes
kindN = \Markup.kindN\
{- formal entities -}
bindingN :: Bytes
bindingN = \Markup.bindingN\
binding :: T
binding = markup_elem bindingN
entityN :: Bytes
entityN = \Markup.entityN\
entity :: Bytes -> Bytes -> T
entity kind name =
(entityN,
(if Bytes.null name then [] else [(nameN, name)]) <>
(if Bytes.null kind then [] else [(kindN, kind)]))
defN :: Bytes
defN = \Markup.defN\
refN :: Bytes
refN = \Markup.refN\
{- completion -}
completionN :: Bytes
completionN = \Markup.completionN\
completion :: T
completion = markup_elem completionN
no_completionN :: Bytes
no_completionN = \Markup.no_completionN\
no_completion :: T
no_completion = markup_elem no_completionN
{- position -}
lineN, end_lineN :: Bytes
lineN = \Markup.lineN\
end_lineN = \Markup.end_lineN\
offsetN, end_offsetN :: Bytes
offsetN = \Markup.offsetN\
end_offsetN = \Markup.end_offsetN\
fileN, idN :: Bytes
fileN = \Markup.fileN\
idN = \Markup.idN\
positionN :: Bytes
positionN = \Markup.positionN\
position :: T
position = markup_elem positionN
position_properties :: [Bytes]
position_properties = [lineN, offsetN, end_offsetN, fileN, idN]
{- position "def" names -}
make_def :: Bytes -> Bytes
make_def a = "def_" <> a
def_names :: Map Bytes Bytes
def_names = Map.fromList $ map (\a -> (a, make_def a)) position_properties
def_name :: Bytes -> Bytes
def_name a =
case Map.lookup a def_names of
Just b -> b
Nothing -> make_def a
{- expression -}
expressionN :: Bytes
expressionN = \Markup.expressionN\
expression :: Bytes -> T
expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
{- citation -}
citationN :: Bytes
citationN = \Markup.citationN\
citation :: Bytes -> T
citation = markup_string nameN citationN
{- external resources -}
pathN :: Bytes
pathN = \Markup.pathN\
path :: Bytes -> T
path = markup_string pathN nameN
urlN :: Bytes
urlN = \Markup.urlN\
url :: Bytes -> T
url = markup_string urlN nameN
docN :: Bytes
docN = \Markup.docN\
doc :: Bytes -> T
doc = markup_string docN nameN
{- pretty printing -}
markupN, consistentN, unbreakableN, indentN :: Bytes
markupN = \Markup.markupN\
consistentN = \Markup.consistentN\
unbreakableN = \Markup.unbreakableN\
indentN = \Markup.indentN\
widthN :: Bytes
widthN = \Markup.widthN\
blockN :: Bytes
blockN = \Markup.blockN\
block :: Bool -> Int -> T
block c i =
(blockN,
(if c then [(consistentN, Value.print_bool c)] else []) <>
(if i /= 0 then [(indentN, Value.print_int i)] else []))
breakN :: Bytes
breakN = \Markup.breakN\
break :: Int -> Int -> T
break w i =
(breakN,
(if w /= 0 then [(widthN, Value.print_int w)] else []) <>
(if i /= 0 then [(indentN, Value.print_int i)] else []))
fbreakN :: Bytes
fbreakN = \Markup.fbreakN\
fbreak :: T
fbreak = markup_elem fbreakN
itemN :: Bytes
itemN = \Markup.itemN\
item :: T
item = markup_elem itemN
{- text properties -}
wordsN :: Bytes
wordsN = \Markup.wordsN\
words :: T
words = markup_elem wordsN
{- inner syntax -}
tfreeN :: Bytes
tfreeN = \Markup.tfreeN\
tfree :: T
tfree = markup_elem tfreeN
tvarN :: Bytes
tvarN = \Markup.tvarN\
tvar :: T
tvar = markup_elem tvarN
freeN :: Bytes
freeN = \Markup.freeN\
free :: T
free = markup_elem freeN
skolemN :: Bytes
skolemN = \Markup.skolemN\
skolem :: T
skolem = markup_elem skolemN
boundN :: Bytes
boundN = \Markup.boundN\
bound :: T
bound = markup_elem boundN
varN :: Bytes
varN = \Markup.varN\
var :: T
var = markup_elem varN
numeralN :: Bytes
numeralN = \Markup.numeralN\
numeral :: T
numeral = markup_elem numeralN
literalN :: Bytes
literalN = \Markup.literalN\
literal :: T
literal = markup_elem literalN
delimiterN :: Bytes
delimiterN = \Markup.delimiterN\
delimiter :: T
delimiter = markup_elem delimiterN
inner_stringN :: Bytes
inner_stringN = \Markup.inner_stringN\
inner_string :: T
inner_string = markup_elem inner_stringN
inner_cartoucheN :: Bytes
inner_cartoucheN = \Markup.inner_cartoucheN\
inner_cartouche :: T
inner_cartouche = markup_elem inner_cartoucheN
token_rangeN :: Bytes
token_rangeN = \Markup.token_rangeN\
token_range :: T
token_range = markup_elem token_rangeN
sortingN :: Bytes
sortingN = \Markup.sortingN\
sorting :: T
sorting = markup_elem sortingN
typingN :: Bytes
typingN = \Markup.typingN\
typing :: T
typing = markup_elem typingN
class_parameterN :: Bytes
class_parameterN = \Markup.class_parameterN\
class_parameter :: T
class_parameter = markup_elem class_parameterN
{- antiquotations -}
antiquotedN :: Bytes
antiquotedN = \Markup.antiquotedN\
antiquoted :: T
antiquoted = markup_elem antiquotedN
antiquoteN :: Bytes
antiquoteN = \Markup.antiquoteN\
antiquote :: T
antiquote = markup_elem antiquoteN
{- text structure -}
paragraphN :: Bytes
paragraphN = \Markup.paragraphN\
paragraph :: T
paragraph = markup_elem paragraphN
text_foldN :: Bytes
text_foldN = \Markup.text_foldN\
text_fold :: T
text_fold = markup_elem text_foldN
{- outer syntax -}
keyword1N :: Bytes
keyword1N = \Markup.keyword1N\
keyword1 :: T
keyword1 = markup_elem keyword1N
keyword2N :: Bytes
keyword2N = \Markup.keyword2N\
keyword2 :: T
keyword2 = markup_elem keyword2N
keyword3N :: Bytes
keyword3N = \Markup.keyword3N\
keyword3 :: T
keyword3 = markup_elem keyword3N
quasi_keywordN :: Bytes
quasi_keywordN = \Markup.quasi_keywordN\
quasi_keyword :: T
quasi_keyword = markup_elem quasi_keywordN
improperN :: Bytes
improperN = \Markup.improperN\
improper :: T
improper = markup_elem improperN
operatorN :: Bytes
operatorN = \Markup.operatorN\
operator :: T
operator = markup_elem operatorN
stringN :: Bytes
stringN = \Markup.stringN\
string :: T
string = markup_elem stringN
alt_stringN :: Bytes
alt_stringN = \Markup.alt_stringN\
alt_string :: T
alt_string = markup_elem alt_stringN
verbatimN :: Bytes
verbatimN = \Markup.verbatimN\
verbatim :: T
verbatim = markup_elem verbatimN
cartoucheN :: Bytes
cartoucheN = \Markup.cartoucheN\
cartouche :: T
cartouche = markup_elem cartoucheN
commentN :: Bytes
commentN = \Markup.commentN\
comment :: T
comment = markup_elem commentN
{- comments -}
comment1N :: Bytes
comment1N = \Markup.comment1N\
comment1 :: T
comment1 = markup_elem comment1N
comment2N :: Bytes
comment2N = \Markup.comment2N\
comment2 :: T
comment2 = markup_elem comment2N
comment3N :: Bytes
comment3N = \Markup.comment3N\
comment3 :: T
comment3 = markup_elem comment3N
{- command status -}
forkedN, joinedN, runningN, finishedN, failedN, canceledN,
initializedN, finalizedN, consolidatedN :: Bytes
forkedN = \Markup.forkedN\
joinedN = \Markup.joinedN\
runningN = \Markup.runningN\
finishedN = \Markup.finishedN\
failedN = \Markup.failedN\
canceledN = \Markup.canceledN\
initializedN = \Markup.initializedN\
finalizedN = \Markup.finalizedN\
consolidatedN = \Markup.consolidatedN\
forked, joined, running, finished, failed, canceled,
initialized, finalized, consolidated :: T
forked = markup_elem forkedN
joined = markup_elem joinedN
running = markup_elem runningN
finished = markup_elem finishedN
failed = markup_elem failedN
canceled = markup_elem canceledN
initialized = markup_elem initializedN
finalized = markup_elem finalizedN
consolidated = markup_elem consolidatedN
{- messages -}
writelnN :: Bytes
writelnN = \Markup.writelnN\
writeln :: T
writeln = markup_elem writelnN
stateN :: Bytes
stateN = \Markup.stateN\
state :: T
state = markup_elem stateN
informationN :: Bytes
informationN = \Markup.informationN\
information :: T
information = markup_elem informationN
tracingN :: Bytes
tracingN = \Markup.tracingN\
tracing :: T
tracing = markup_elem tracingN
warningN :: Bytes
warningN = \Markup.warningN\
warning :: T
warning = markup_elem warningN
legacyN :: Bytes
legacyN = \Markup.legacyN\
legacy :: T
legacy = markup_elem legacyN
errorN :: Bytes
errorN = \Markup.errorN\
error :: T
error = markup_elem errorN
reportN :: Bytes
reportN = \Markup.reportN\
report :: T
report = markup_elem reportN
no_reportN :: Bytes
no_reportN = \Markup.no_reportN\
no_report :: T
no_report = markup_elem no_reportN
intensifyN :: Bytes
intensifyN = \Markup.intensifyN\
intensify :: T
intensify = markup_elem intensifyN
{- output -}
type Output = (Bytes, Bytes)
no_output :: Output
no_output = ("", "")
\
generate_file "Isabelle/Position.hs" = \
{- Title: Isabelle/Position.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
right-open interval offset .. end_offset (exclusive).
See \<^file>\$ISABELLE_HOME/src/Pure/General/position.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
module Isabelle.Position (
T, line_of, column_of, offset_of, end_offset_of, file_of, id_of,
start, none, put_file, file, file_only, put_id, id, id_only,
symbol, symbol_explode, symbol_explode_string, shift_offsets,
of_properties, properties_of, def_properties_of, entity_markup, make_entity_markup,
Report, Report_Text, is_reported, is_reported_range, here,
Range, no_range, no_range_position, range_position, range
)
where
import Prelude hiding (id)
import Data.Maybe (isJust, fromMaybe)
import Data.Bifunctor (first)
import qualified Isabelle.Properties as Properties
import qualified Isabelle.Bytes as Bytes
import qualified Isabelle.Value as Value
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Markup as Markup
import qualified Isabelle.YXML as YXML
import Isabelle.Library
import qualified Isabelle.Symbol as Symbol
import Isabelle.Symbol (Symbol)
{- position -}
data T =
Position {
_line :: Int,
_column :: Int,
_offset :: Int,
_end_offset :: Int,
_file :: Bytes,
_id :: Bytes }
deriving (Eq, Ord)
valid, invalid :: Int -> Bool
valid i = i > 0
invalid = not . valid
maybe_valid :: Int -> Maybe Int
maybe_valid i = if valid i then Just i else Nothing
if_valid :: Int -> Int -> Int
if_valid i i' = if valid i then i' else i
{- fields -}
line_of, column_of, offset_of, end_offset_of :: T -> Maybe Int
line_of = maybe_valid . _line
column_of = maybe_valid . _column
offset_of = maybe_valid . _offset
end_offset_of = maybe_valid . _end_offset
file_of :: T -> Maybe Bytes
file_of = proper_string . _file
id_of :: T -> Maybe Bytes
id_of = proper_string . _id
{- make position -}
start :: T
start = Position 1 1 1 0 Bytes.empty Bytes.empty
none :: T
none = Position 0 0 0 0 Bytes.empty Bytes.empty
put_file :: Bytes -> T -> T
put_file file pos = pos { _file = file }
file :: Bytes -> T
file file = put_file file start
file_only :: Bytes -> T
file_only file = put_file file none
put_id :: Bytes -> T -> T
put_id id pos = pos { _id = id }
id :: Bytes -> T
id id = put_id id start
id_only :: Bytes -> T
id_only id = put_id id none
{- count position -}
count_line :: Symbol -> Int -> Int
count_line "\n" line = if_valid line (line + 1)
count_line _ line = line
count_column :: Symbol -> Int -> Int
count_column "\n" column = if_valid column 1
count_column s column = if Symbol.not_eof s then if_valid column (column + 1) else column
count_offset :: Symbol -> Int -> Int
count_offset s offset = if Symbol.not_eof s then if_valid offset (offset + 1) else offset
symbol :: Symbol -> T -> T
symbol s pos =
pos {
_line = count_line s (_line pos),
_column = count_column s (_column pos),
_offset = count_offset s (_offset pos) }
symbol_explode :: BYTES a => a -> T -> T
symbol_explode = fold symbol . Symbol.explode . make_bytes
symbol_explode_string :: String -> T -> T
symbol_explode_string = symbol_explode
{- shift offsets -}
shift_offsets :: Int -> T -> T
shift_offsets shift pos = pos { _offset = offset', _end_offset = end_offset' }
where
offset = _offset pos
end_offset = _end_offset pos
offset' = if invalid offset || invalid shift then offset else offset + shift
end_offset' = if invalid end_offset || invalid shift then end_offset else end_offset + shift
{- markup properties -}
get_string :: Properties.T -> Bytes -> Bytes
get_string props name = fromMaybe "" (Properties.get_value Just props name)
get_int :: Properties.T -> Bytes -> Int
get_int props name = fromMaybe 0 (Properties.get_value Value.parse_int props name)
of_properties :: Properties.T -> T
of_properties props =
none {
_line = get_int props Markup.lineN,
_offset = get_int props Markup.offsetN,
_end_offset = get_int props Markup.end_offsetN,
_file = get_string props Markup.fileN,
_id = get_string props Markup.idN }
string_entry :: Bytes -> Bytes -> Properties.T
string_entry k s = if Bytes.null s then [] else [(k, s)]
int_entry :: Bytes -> Int -> Properties.T
int_entry k i = if invalid i then [] else [(k, Value.print_int i)]
properties_of :: T -> Properties.T
properties_of pos =
int_entry Markup.lineN (_line pos) ++
int_entry Markup.offsetN (_offset pos) ++
int_entry Markup.end_offsetN (_end_offset pos) ++
string_entry Markup.fileN (_file pos) ++
string_entry Markup.idN (_id pos)
def_properties_of :: T -> Properties.T
def_properties_of = properties_of #> map (first Markup.def_name)
entity_markup :: Bytes -> (Bytes, T) -> Markup.T
entity_markup kind (name, pos) =
Markup.entity kind name |> Markup.properties (def_properties_of pos)
make_entity_markup :: Bool -> Int -> Bytes -> (Bytes, T) -> Markup.T
make_entity_markup def serial kind (name, pos) =
let
props =
if def then (Markup.defN, Value.print_int serial) : properties_of pos
else (Markup.refN, Value.print_int serial) : def_properties_of pos
in Markup.entity kind name |> Markup.properties props
{- reports -}
type Report = (T, Markup.T)
type Report_Text = (Report, Bytes)
is_reported :: T -> Bool
is_reported pos = isJust (offset_of pos) && isJust (id_of pos)
is_reported_range :: T -> Bool
is_reported_range pos = is_reported pos && isJust (end_offset_of pos)
{- here: user output -}
here :: T -> Bytes
here pos = if Bytes.null s2 then "" else s1 <> m1 <> s2 <> m2
where
props = properties_of pos
(m1, m2) = YXML.output_markup (Markup.properties props Markup.position)
(s1, s2) =
case (line_of pos, file_of pos) of
(Just i, Nothing) -> (" ", "(line " <> Value.print_int i <> ")")
(Just i, Just name) -> (" ", "(line " <> Value.print_int i <> " of " <> quote name <> ")")
(Nothing, Just name) -> (" ", "(file " <> quote name <> ")")
_ -> if is_reported pos then ("", "\092<^here>") else ("", "")
{- range -}
type Range = (T, T)
no_range :: Range
no_range = (none, none)
no_range_position :: T -> T
no_range_position pos = pos { _end_offset = 0 }
range_position :: Range -> T
range_position (pos, pos') = pos { _end_offset = _offset pos' }
range :: Range -> Range
range (pos, pos') = (range_position (pos, pos'), no_range_position pos')
\
generate_file "Isabelle/XML.hs" = \
{- Title: Isabelle/XML.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Untyped XML trees and representation of ML values.
See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
where
import Isabelle.Library
import qualified Isabelle.Properties as Properties
import qualified Isabelle.Markup as Markup
import qualified Isabelle.Buffer as Buffer
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
{- types -}
type Attributes = Properties.T
type Body = [Tree]
data Tree = Elem (Markup.T, Body) | Text Bytes
{- wrapped elements -}
wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree
wrap_elem (((a, atts), body1), body2) =
Elem ((\XML.xml_elemN\, (\XML.xml_nameN\, a) : atts), Elem ((\XML.xml_bodyN\, []), body1) : body2)
unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree])
unwrap_elem
(Elem ((\XML.xml_elemN\, (\XML.xml_nameN\, a) : atts), Elem ((\XML.xml_bodyN\, []), body1) : body2)) =
Just (((a, atts), body1), body2)
unwrap_elem _ = Nothing
{- text content -}
add_content :: Tree -> Buffer.T -> Buffer.T
add_content tree =
case unwrap_elem tree of
Just (_, ts) -> fold add_content ts
Nothing ->
case tree of
Elem (_, ts) -> fold add_content ts
Text s -> Buffer.add s
content_of :: Body -> Bytes
-content_of body = Buffer.empty |> fold add_content body |> Buffer.content
+content_of = Buffer.build_content . fold add_content
{- string representation -}
encode_char :: Char -> String
encode_char '<' = "<"
encode_char '>' = ">"
encode_char '&' = "&"
encode_char '\'' = "'"
encode_char '\"' = """
encode_char c = [c]
encode_text :: Bytes -> Bytes
encode_text = make_bytes . concatMap (encode_char . Bytes.char) . Bytes.unpack
instance Show Tree where
show tree =
- Buffer.empty |> show_tree tree |> Buffer.content |> make_string
+ make_string $ Buffer.build_content (show_tree tree)
where
show_tree (Elem ((name, atts), [])) =
Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
show_tree (Elem ((name, atts), ts)) =
Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
fold show_tree ts #>
Buffer.add " Buffer.add name #> Buffer.add ">"
show_tree (Text s) = Buffer.add (encode_text s)
show_elem name atts =
space_implode " " (name : map (\(a, x) -> a <> "=\"" <> encode_text x <> "\"") atts)
\
generate_file "Isabelle/XML/Encode.hs" = \
{- Title: Isabelle/XML/Encode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
XML as data representation language.
See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Isabelle.XML.Encode (
A, T, V, P,
int_atom, bool_atom, unit_atom,
tree, properties, string, int, bool, unit, pair, triple, list, option, variant
)
where
import Data.Maybe (fromJust)
import Isabelle.Library
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Value as Value
import qualified Isabelle.Properties as Properties
import qualified Isabelle.XML as XML
type A a = a -> Bytes
type T a = a -> XML.Body
type V a = a -> Maybe ([Bytes], XML.Body)
type P a = a -> [Bytes]
-- atomic values
int_atom :: A Int
int_atom = Value.print_int
bool_atom :: A Bool
bool_atom False = "0"
bool_atom True = "1"
unit_atom :: A ()
unit_atom () = ""
-- structural nodes
node ts = XML.Elem ((":", []), ts)
vector = map_index (\(i, x) -> (int_atom i, x))
tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)
-- representation of standard types
tree :: T XML.Tree
tree t = [t]
properties :: T Properties.T
properties props = [XML.Elem ((":", props), [])]
string :: T Bytes
string "" = []
string s = [XML.Text s]
int :: T Int
int = string . int_atom
bool :: T Bool
bool = string . bool_atom
unit :: T ()
unit = string . unit_atom
pair :: T a -> T b -> T (a, b)
pair f g (x, y) = [node (f x), node (g y)]
triple :: T a -> T b -> T c -> T (a, b, c)
triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
list :: T a -> T [a]
list f xs = map (node . f) xs
option :: T a -> T (Maybe a)
option _ Nothing = []
option f (Just x) = [node (f x)]
variant :: [V a] -> T a
variant fs x = [tagged (fromJust (get_index (\f -> f x) fs))]
\
generate_file "Isabelle/XML/Decode.hs" = \
{- Title: Isabelle/XML/Decode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
XML as data representation language.
See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Isabelle.XML.Decode (
A, T, V, P,
int_atom, bool_atom, unit_atom,
tree, properties, string, int, bool, unit, pair, triple, list, option, variant
)
where
import Isabelle.Library
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Value as Value
import qualified Isabelle.Properties as Properties
import qualified Isabelle.XML as XML
type A a = Bytes -> a
type T a = XML.Body -> a
type V a = ([Bytes], XML.Body) -> a
type P a = [Bytes] -> a
err_atom = error "Malformed XML atom"
err_body = error "Malformed XML body"
{- atomic values -}
int_atom :: A Int
int_atom s =
case Value.parse_int s of
Just i -> i
Nothing -> err_atom
bool_atom :: A Bool
bool_atom "0" = False
bool_atom "1" = True
bool_atom _ = err_atom
unit_atom :: A ()
unit_atom "" = ()
unit_atom _ = err_atom
{- structural nodes -}
node (XML.Elem ((":", []), ts)) = ts
node _ = err_body
vector atts =
map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
tagged _ = err_body
{- representation of standard types -}
tree :: T XML.Tree
tree [t] = t
tree _ = err_body
properties :: T Properties.T
properties [XML.Elem ((":", props), [])] = props
properties _ = err_body
string :: T Bytes
string [] = ""
string [XML.Text s] = s
string _ = err_body
int :: T Int
int = int_atom . string
bool :: T Bool
bool = bool_atom . string
unit :: T ()
unit = unit_atom . string
pair :: T a -> T b -> T (a, b)
pair f g [t1, t2] = (f (node t1), g (node t2))
pair _ _ _ = err_body
triple :: T a -> T b -> T c -> T (a, b, c)
triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
triple _ _ _ _ = err_body
list :: T a -> T [a]
list f ts = map (f . node) ts
option :: T a -> T (Maybe a)
option _ [] = Nothing
option f [t] = Just (f (node t))
option _ _ = err_body
variant :: [V a] -> T a
variant fs [t] = (fs !! tag) (xs, ts)
where (tag, (xs, ts)) = tagged t
variant _ _ = err_body
\
generate_file "Isabelle/YXML.hs" = \
{- Title: Isabelle/YXML.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Efficient text representation of XML trees. Suitable for direct
inlining into plain text.
See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-incomplete-patterns #-}
module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
buffer_body, buffer, string_of_body, string_of, parse_body, parse)
where
import qualified Data.List as List
import Data.Word (Word8)
import Isabelle.Library
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Markup as Markup
import qualified Isabelle.XML as XML
import qualified Isabelle.Buffer as Buffer
{- markers -}
charX, charY :: Word8
charX = 5
charY = 6
strX, strY, strXY, strXYX :: Bytes
strX = Bytes.singleton charX
strY = Bytes.singleton charY
strXY = strX <> strY
strXYX = strXY <> strX
detect :: Bytes -> Bool
detect = Bytes.any (\c -> c == charX || c == charY)
{- output -}
output_markup :: Markup.T -> Markup.Output
output_markup markup@(name, atts) =
if Markup.is_empty markup then Markup.no_output
else (strXY <> name <> Bytes.concat (map (\(a, x) -> strY <> a <> "=" <> x) atts) <> strX, strXYX)
buffer_attrib (a, x) =
Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
buffer_body :: XML.Body -> Buffer.T -> Buffer.T
buffer_body = fold buffer
buffer :: XML.Tree -> Buffer.T -> Buffer.T
buffer (XML.Elem ((name, atts), ts)) =
Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
buffer_body ts #>
Buffer.add strXYX
buffer (XML.Text s) = Buffer.add s
string_of_body :: XML.Body -> Bytes
-string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
+string_of_body = Buffer.build_content . buffer_body
string_of :: XML.Tree -> Bytes
string_of = string_of_body . single
{- parse -}
-- split: fields or non-empty tokens
split :: Bool -> Word8 -> [Word8] -> [[Word8]]
split _ _ [] = []
split fields sep str = splitting str
where
splitting rest =
case span (/= sep) rest of
(_, []) -> cons rest []
(prfx, _ : rest') -> cons prfx (splitting rest')
cons item = if fields || not (null item) then (:) item else id
-- structural errors
err :: Bytes -> a
err msg = error (make_string ("Malformed YXML: " <> msg))
err_attribute = err "bad attribute"
err_element = err "bad element"
err_unbalanced :: Bytes -> a
err_unbalanced name =
if Bytes.null name then err "unbalanced element"
else err ("unbalanced element " <> quote name)
-- stack operations
add x ((elem, body) : pending) = (elem, x : body) : pending
push name atts pending =
if Bytes.null name then err_element
else ((name, atts), []) : pending
pop (((name, atts), body) : pending) =
if Bytes.null name then err_unbalanced name
else add (XML.Elem ((name, atts), reverse body)) pending
-- parsing
parse_attrib s =
case List.elemIndex (Bytes.byte '=') s of
Just i | i > 0 -> (Bytes.pack $ take i s, Bytes.pack $ drop (i + 1) s)
_ -> err_attribute
parse_chunk [[], []] = pop
parse_chunk ([] : name : atts) = push (Bytes.pack name) (map parse_attrib atts)
parse_chunk txts = fold (add . XML.Text . Bytes.pack) txts
parse_body :: Bytes -> XML.Body
parse_body source =
case fold parse_chunk chunks [((Bytes.empty, []), [])] of
[((name, _), result)] | Bytes.null name -> reverse result
((name, _), _) : _ -> err_unbalanced name
where chunks = source |> Bytes.unpack |> split False charX |> map (split True charY)
parse :: Bytes -> XML.Tree
parse source =
case parse_body source of
[result] -> result
[] -> XML.Text ""
_ -> err "multiple results"
\
generate_file "Isabelle/Completion.hs" = \
{- Title: Isabelle/Completion.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Completion of names.
See \<^file>\$ISABELLE_HOME/src/Pure/General/completion.ML\.
-}
{-# LANGUAGE OverloadedStrings #-}
module Isabelle.Completion (
Name, T, names, none, make, markup_element, markup_report, make_report
) where
import qualified Isabelle.Bytes as Bytes
import qualified Isabelle.Name as Name
import Isabelle.Name (Name)
import qualified Isabelle.Properties as Properties
import qualified Isabelle.Markup as Markup
import Isabelle.XML.Classes
import qualified Isabelle.XML as XML
import qualified Isabelle.YXML as YXML
type Names = [(Name, (Name, Name))] -- external name, kind, internal name
data T = Completion Properties.T Int Names -- position, total length, names
names :: Int -> Properties.T -> Names -> T
names limit props names = Completion props (length names) (take limit names)
none :: T
none = names 0 [] []
make :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> T
make limit (name, props) make_names =
if name /= "" && name /= "_" then
names limit props (make_names (Bytes.isPrefixOf (Name.clean name)))
else none
markup_element :: T -> (Markup.T, XML.Body)
markup_element (Completion props total names) =
if not (null names) then
(Markup.properties props Markup.completion, encode (total, names))
else (Markup.empty, [])
markup_report :: [T] -> Name
markup_report [] = Bytes.empty
markup_report elems =
YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
make_report :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> Name
make_report limit name_props make_names =
markup_report [make limit name_props make_names]
\
generate_file "Isabelle/File.hs" = \
{- Title: Isabelle/File.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
File-system operations.
See \<^file>\$ISABELLE_HOME/src/Pure/General/file.ML\.
-}
module Isabelle.File (read, write, append) where
import Prelude hiding (read)
import qualified System.IO as IO
import qualified Data.ByteString as ByteString
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
read :: IO.FilePath -> IO Bytes
read path = Bytes.make <$> IO.withFile path IO.ReadMode ByteString.hGetContents
write :: IO.FilePath -> Bytes -> IO ()
write path bs = IO.withFile path IO.WriteMode (\h -> ByteString.hPut h (Bytes.unmake bs))
append :: IO.FilePath -> Bytes -> IO ()
append path bs = IO.withFile path IO.AppendMode (\h -> ByteString.hPut h (Bytes.unmake bs))
\
generate_file "Isabelle/Pretty.hs" = \
{- Title: Isabelle/Pretty.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Generic pretty printing module.
See \<^file>\