wip

src/Explication.ml

@@ -1,17 +1,19 @@
 include ExplicationData
 
-let dump_marker dump_tag fmt = function
+let dump_marker dump_tag fmt =
+  function
   | RangeBegin tag -> Format.fprintf fmt {|@[<2>RangeBegin@ @[%a@]@]|} dump_tag tag
   | RangeEnd tag -> Format.fprintf fmt {|@[<2>RangeEnd@ @[%a@]@]|} dump_tag tag
   | Point tag -> Format.fprintf fmt {|@[<2>Point@ @[%a@]@]|} dump_tag tag
 
-let dump_token dump_tag fmt = function
+let dump_token dump_tag fmt =
+  function
   | String str -> Format.fprintf fmt {|@[<2>String@ "%s"@]|} (String.escaped str)
   | Marker m -> Format.fprintf fmt {|@[<2>Marker@ @[<1>(%a)@]@]|} (dump_marker dump_tag) m
 
-let dump_line dump_tag fmt {tags; tokens} =
+let dump_line dump_tag fmt {markers; tokens} =
   Format.fprintf fmt {|@[<1>{@[<2>tags=@,@[%a@]@];@ @[<2>tokens=@ @[%a@]@]}@]|}
-    (Utils.dump_list dump_tag) tags
+    (Utils.dump_list dump_tag) markers
     (Utils.dump_list (dump_token dump_tag)) tokens
 
 let dump_block dump_tag fmt {begin_line_num; end_line_num; lines} =

src/ExplicationData.ml

@@ -11,7 +11,7 @@ type 'tag token =
 
 (** A line is a list of {!type:segment}s along with tags. *)
 type 'tag line =
-  { tags : 'tag list (** All tags in this line *)
+  { markers : 'tag list (** All tags in this line *)
   ; tokens : 'tag token list
   }
 

src/Explicator.ml

@@ -30,9 +30,6 @@ let print_invalid_range fmt : UserContent.invalid_range -> unit =
     Format.fprintf fmt "its@ beginning@ position@ is@ invalid;@ %a" print_invalid_position r
   | `End r ->
     Format.fprintf fmt "its@ ending@ position@ is@ invalid;@ %a" print_invalid_position r
-  | `Not_end_of_file (l, l') ->
-    Format.fprintf fmt "its@ offset@ %d@ is@ not@ the@ end@ of@ file@ (%d)." l l'
-  | `End_of_file r -> print_invalid_position fmt r
 
 let () = Printexc.register_printer @@
   function
@@ -74,11 +71,11 @@ module Make (Tag : Tag) = struct
 
   module F = Flattener.Make(Tag)
 
-  let explicate_block ~line_breaks (b : Tag.t Flattener.block) : Tag.t block =
+  let explicate_block ~line_breaks source (b : Tag.t Flattener.block) : Tag.t block =
     match b.markers with
     | [] -> invalid_arg "explicate_block: empty block; should be impossible"
     | ((first_loc, _) :: _) as markers ->
-      let source = SourceReader.load first_loc.source in
+      let source = SourceReader.load source in
       let eof = SourceReader.length source in
       let find_eol i = UserContent.find_eol ~line_breaks (SourceReader.unsafe_get source) (i, eof) in
       let rec go state : (Range.position * Tag.t marker) list -> _ =
@@ -93,7 +90,7 @@ module Make (Tag : Tag) = struct
               state.tokens <: String (read_between ~source state.cursor.offset loc.offset) <: Marker marker
           in
           go { state with tokens; cursor = loc } markers
-        | ps ->
+        | markers ->
           (* Shifting to the next line *)
           let lines, remaining_line_markers =
             let tokens =
@@ -105,10 +102,14 @@ module Make (Tag : Tag) = struct
             let line_markers, remaining_line_markers =
               Utils.span (fun (line_num, _) -> line_num = state.line_num) state.remaining_line_markers
             in
-            (state.lines <: {tokens = Bwd.to_list tokens; tags = List.map snd line_markers}), remaining_line_markers
+            (state.lines <:
+             { tokens = Bwd.to_list tokens
+             ; markers = List.map snd line_markers
+             }),
+            remaining_line_markers
           in
-          (* Continue the process if [ps] is not empty. *)
-          match ps, state.eol_shift with
+          (* Continue the process if [markers] is not empty. *)
+          match markers, state.eol_shift with
           | [], _ ->
             assert (state.line_num = b.end_line_num);
             lines
@@ -129,11 +130,11 @@ module Make (Tag : Tag) = struct
               ; eol_shift
               ; line_num = state.line_num + 1
               }
-              ps
+              markers
       in
-      let begin_pos = to_start_of_line first_loc in
-      let eol, eol_shift = find_eol first_loc.offset in
       let lines =
+        let begin_pos = to_start_of_line first_loc in
+        let eol, eol_shift = find_eol first_loc.offset in
         go
           { lines = Emp
           ; tokens = Emp
@@ -150,10 +151,11 @@ module Make (Tag : Tag) = struct
       ; lines = Bwd.to_list @@ lines
       }
 
-  let[@inline] explicate_blocks ~line_breaks = List.map (explicate_block ~line_breaks)
+  let[@inline] explicate_blocks ~line_breaks source ranges =
+    List.map (explicate_block ~line_breaks source) ranges
 
   let[@inline] explicate_part ~line_breaks (source, bs) : Tag.t part =
-    { source; blocks = explicate_blocks ~line_breaks bs }
+    { source; blocks = explicate_blocks ~line_breaks source bs }
 
   let check_ranges ~line_breaks ranges =
     List.iter

src/Flattener.ml

@@ -37,8 +37,7 @@ struct
     ; ranges : (Range.t * Tag.t) bwd}
 
   let compare_position (p1 : Range.position) (p2 : Range.position) =
-    Utils.compare_pair Int.compare Int.compare
-      (p1.offset, p1.line_num) (p2.offset, p2.line_num)
+    Int.compare p1.offset p2.offset
 
   (* Stage 1: group ranges into blocks *)
   module Splitter :
@@ -87,7 +86,21 @@ struct
       partition_sorted ~block_splitting_threshold (sort_tagged l)
   end
 
-  (* Stage 2: flatten out ranges into tokens *)
+  (* Stage 2: flatten out ranges into markers
+
+     The code needs to handle several subtleties, using the XML-like notation to demonstrate:
+     1. The ordering of markers and text strings should be ordered like this:
+        <range1>...</range1><point/><range2>...</range2>
+        Note that, in the middle, RangeEnd goes first, and then Point, and then RangeBegin.
+     2. If the set of ranges is "well-scoped" (that is, a range is always completely included in,
+        completely including, or being disjoint from another range), then matching beginning and
+        ending markers will have the expected nested structures, like this:
+        <range1><range2>...</range2><range3>...</range3></range1>
+     3. For two ranges marking the same text with different priorities, the prioritized one goes inside.
+        For two ranges with the same text and priority, the order of beginning markers will follow
+        the order of the original input list. This is to reduce interruption of the prioritized highlighting.
+        <low_pri1><low_pri2><high_pri1><high_pri2>...</high_pri2></high_pri1></low_pri2></low_pri1>
+  *)
   module BlockFlattener :
   sig
     val flatten : (Range.t * Tag.t) list -> (Range.position * Tag.t marker) list
@@ -96,29 +109,33 @@ struct
   struct
     type t =
       { begins : (Range.position * Tag.t marker) bwd
-      ; points : (Range.position * Tag.t marker) list
+      ; points : (Range.position * Tag.t marker) bwd
       ; ends : (Range.position * Tag.t marker) list
       }
 
     let add {begins; points; ends} (range, tag) =
       let b, e = Range.split range in
       if compare_position b e = 0 then
-        {begins; points = (b, Point tag) :: points; ends}
+        {begins; points = points <: (b, Point tag); ends}
       else
         {begins = begins <: (b, RangeBegin tag); points; ends = (e, RangeEnd tag) :: ends}
 
-    let sort_cmd =
-      let compare_cmd (p1, _) (p2, _) =
-        compare_position p1 p2
+    let sort_marker =
+      let marker_order =
+        function
+        | RangeEnd _ -> -1
+        | Point _ -> 0
+        | RangeBegin _ -> 1
       in
-      List.stable_sort compare_cmd
+      let compare_marker m1 m2 = Int.compare (marker_order m1) (marker_order m2) in
+      List.stable_sort (Utils.compare_pair compare_position compare_marker)
 
-    let merge_cmd {begins; points; ends} =
-      (begins <@ points) @> ends
+    let merge_marker {begins; points; ends} =
+      begins @> points @> ends
 
     let flatten l =
-      sort_cmd @@ merge_cmd @@
-      List.fold_left add {begins = Emp; points = []; ends = []} l
+      sort_marker @@ merge_marker @@
+      List.fold_left add {begins = Emp; points = Emp; ends = []} l
   end
 
   module FileFlattener :

src/UserContent.ml

@@ -80,13 +80,9 @@ let check_pos ~line_breaks ~eof read pos =
     raise @@ Invalid_position (`Incorrect_start_of_line (pos.start_of_line, new_pos.start_of_line))
 
 let check_range ~line_breaks ~eof read range =
-  match Range.view range with
-  | `Range (p1, p2) ->
-    (try check_pos ~line_breaks ~eof read p1 with Invalid_position reason -> raise @@ Invalid_range (`Begin reason));
-    (try check_pos ~line_breaks ~eof read p2 with Invalid_position reason -> raise @@ Invalid_range (`End reason))
-  | `End_of_file p ->
-    if p.offset <> eof then raise @@ Invalid_range (`Not_end_of_file (p.offset, eof));
-    (try check_pos ~line_breaks ~eof read p with Invalid_position reason -> raise @@ Invalid_range (`End_of_file reason))
+  let p1, p2 = Range.split range in
+  (try check_pos ~line_breaks ~eof read p1 with Invalid_position reason -> raise @@ Invalid_range (`Begin reason));
+  (try check_pos ~line_breaks ~eof read p2 with Invalid_position reason -> raise @@ Invalid_range (`End reason))
 
 let replace_control ~tab_size str =
   let tab_string = String.make tab_size ' ' in

src/UserContentData.ml

@@ -16,6 +16,4 @@ type invalid_position =
 type invalid_range =
   [ `Begin of invalid_position (** The first position of a range is invalid. *)
   | `End of invalid_position (** The second position of a range is invalid. *)
-  | `End_of_file of invalid_position (** The range is a special end-of-file marking, but the position is invalid. *)
-  | `Not_end_of_file of int * int (** The range is a special end-of-file marking, but the offset of the position is not at the end of file. The pair [(m, n)] means that the current offset is [m] but the length or size of the source is [n]. *)
   ]

src/tty/Ansi.ml

@@ -105,7 +105,7 @@ struct
 
   let guess ?use_ansi ?use_color o =
     if use_color = Some true && use_ansi = Some false then
-      invalid_arg "Ansi.Tty.display: called with use_color=true but use_ansi=false";
+      invalid_arg "Asai.Tty.S.display: called with use_color=true but use_ansi=false";
     let enabled = match use_ansi with Some a -> a | None -> rich_term && is_tty o in
     let color = enabled && match use_color with Some c -> c | None -> not no_color in
     {enabled; color}

src/tty/Tty.ml

@@ -43,13 +43,13 @@ let indentf ~param fmt =
 (* different parts of the display *)
 
 let render_code ~param ~severity fmt short_code =
-  let st = TtyStyle.code severity ~param in
+  let style = TtyStyle.code severity ~param in
   Format.fprintf fmt (" @<1>%s " ^^ highlight "%s[%s]" ^^ "@.")
     "￫"
-    (Ansi.style_string ~param st)
+    (Ansi.style_string ~param style)
     (string_of_severity severity)
     short_code
-    (Ansi.reset_string ~param st)
+    (Ansi.reset_string ~param style)
 
 (* explication *)
 
@@ -83,35 +83,60 @@ struct
     | None -> ()
     | Some title -> Format.fprintf fmt " @<1>%s %s@." "￭" title
 
-  let render_segment ~param fmt (tag, seg) =
-    let st = TtyStyle.highlight ~param:param.ansi param.severity tag in
-    Format.fprintf fmt (highlight "%s")
-      (Ansi.style_string ~param:param.ansi st)
-      (UserContent.replace_control ~tab_size:param.tab_size seg)
-      (Ansi.reset_string ~param:param.ansi st)
-
   let render_line_marker ~param fmt ((_, text) as tag) =
-    let st = TtyStyle.message ~param:param.ansi param.severity tag in
+    let style = TtyStyle.message ~param:param.ansi param.severity tag in
     Format.fprintf fmt (" %*s " ^^ highlight "^" ^^ " " ^^ highlight "@[%t@]" ^^ "@.")
       param.line_number_width ""
       (Ansi.style_string ~param:param.ansi TtyStyle.fringe)
       (Ansi.reset_string ~param:param.ansi TtyStyle.fringe)
-      (Ansi.style_string ~param:param.ansi st)
+      (Ansi.style_string ~param:param.ansi style)
       text
-      (Ansi.reset_string ~param:param.ansi st)
+      (Ansi.reset_string ~param:param.ansi style)
 
-  let render_line ~line_num ~param fmt Explication.{tokens; tags} =
+  let render_styled_segment ~param fmt tag segment =
+    let style = TtyStyle.highlight ~param:param.ansi param.severity tag in
+    Format.fprintf fmt (highlight "%s")
+      (Ansi.style_string ~param:param.ansi style)
+      (UserContent.replace_control ~tab_size:param.tab_size segment)
+      (Ansi.reset_string ~param:param.ansi style)
+
+  type state = TtyTagSet.t
+
+
+  (* Current design:
+
+     ‹let x◂POS₀▸ = 1› in let ‹x› = «1 + ‹x›»◂POS₁▸
+     ‹let x◂POS₀▸ = 1›₀ in let ‹x›₁ = «1 + ‹x›₂»◂POS₁▸
+  *)
+
+  let render_line ~line_num ~param fmt init_tag_set Explication.{tokens; markers} =
+    let rec go set =
+      function
+      | Explication.String s ->
+        render_styled_segment ~param fmt (TtyTagSet.prioritized set) s; set
+      | Explication.Marker RangeEnd t ->
+        render_styled_segment ~param fmt (Some t) "›"; TtyTagSet.remove t set
+      | Explication.Marker Point t ->
+        render_styled_segment ~param fmt (Some t) "◂POS▸"; set
+      | Explication.Marker RangeBegin t ->
+        render_styled_segment ~param fmt (Some t) "‹"; TtyTagSet.add t set
+    in
     Format.fprintf fmt (" " ^^ highlight "%*d |" ^^ " ")
       (Ansi.style_string ~param:param.ansi TtyStyle.fringe)
       param.line_number_width line_num
       (Ansi.reset_string ~param:param.ansi TtyStyle.fringe);
-    List.iter (render_segment ~param fmt) tokens;
+    let end_tag_set = List.fold_left go init_tag_set tokens in
     Format.fprintf fmt "@.";
-    List.iter (render_line_tag ~param fmt) tags
+    List.iter (render_line_marker ~param fmt) markers;
+    end_tag_set
 
   let render_lines ~param ~begin_line_num fmt lines =
-    lines |> List.iteri @@ fun i line ->
-    render_line ~line_num:(begin_line_num + i) ~param fmt line
+    ignore @@ List.fold_left
+      (fun (line_num, set) line ->
+         let set = render_line ~line_num ~param fmt set line in
+         (line_num+1, set))
+      (begin_line_num, TtyTagSet.empty)
+      lines
 
   let render_block ~param fmt Explication.{begin_line_num; end_line_num=_; lines} =
     render_lines ~param ~begin_line_num fmt lines
@@ -125,12 +150,12 @@ struct
 end
 
 let render_unlocated_tag ~severity ~ansi fmt ((_, text) as tag) =
-  let st = TtyStyle.message ~param:ansi severity tag in
+  let style = TtyStyle.message ~param:ansi severity tag in
   Format.fprintf fmt (" @<1>%s " ^^ highlight "@[%t@]" ^^ "@.")
     "￮"
-    (Ansi.style_string ~param:ansi st)
+    (Ansi.style_string ~param:ansi style)
     text
-    (Ansi.reset_string ~param:ansi st)
+    (Ansi.reset_string ~param:ansi style)
 
 module DiagnosticRenderer :
 sig
@@ -173,7 +198,7 @@ struct
       List.partition_map
         (function
           | (tag, Range.{loc = None; value = text}) -> Either.Right (tag, text)
-          | (tag, Range.{loc = Some r; value = text}) -> Either.Left ((tag, text), r))
+          | (tag, Range.{loc = Some r; value = text}) -> Either.Left (r, (tag, text)))
         (main :: extra_remarks)
     in
     let explication =

src/tty/TtyTag.ml

@@ -4,6 +4,9 @@ let priority =
   function
   | Main, _ -> -1
   | Extra i, _ -> i
+let compare t1 t2 =
+  Utils.compare_pair Int.compare Stdlib.compare
+    (priority t1, t1) (priority t2, t2)
 let dump fmt =
   function
   | Main, _ -> Format.pp_print_string fmt "Main"