go back in time to display holes, so name/notation scope is correct

Author: mikeshulman

lib/core/global.ml

@@ -316,7 +316,7 @@ let add_hole m loc ~vars ~termctx ~ty ~status ~li ~ri =
               ( cmd.current_holes,
                 {
                   meta = Wrap m;
-                  printable = PHole (vars, termctx, ty);
+                  printable = PHole (Origin.current (), vars, termctx, ty);
                   startpos = s.offset;
                   endpos = e.offset;
                 } );

lib/core/printable.ml

@@ -2,6 +2,7 @@ open Util
 open Term
 open Value
 open Reporter
+open Origin
 
 let phead : head -> printable = function
   | Const { name; _ } -> PConstant name
@@ -15,5 +16,5 @@ type printable +=
   | PNormal : ('a, 'b) Ctx.t * normal -> printable
   | (* When printing a hole we use a termctx, since that's what we store anyway, and we would also have to read back a value context anyway in order to unparse it. *)
       PHole :
-      (string option, 'a) Bwv.t * ('a, 'b) termctx * ('b, kinetic) term
+      Origin.t * (string option, 'a) Bwv.t * ('a, 'b) termctx * ('b, kinetic) term
       -> printable

lib/parser/command.ml

@@ -721,8 +721,8 @@ let parse_single (content : string) : Whitespace.t list * Command.t option =
   | _ -> Core.Reporter.fatal (Anomaly "interactive parse doesn't start with Bof")
 
 let show_hole = function
-  | Global.Found_hole { meta; termctx; ty; vars; _ } ->
-      emit (Hole (Meta.name meta, PHole (vars, termctx, ty)))
+  | Global.Found_hole { instant; meta; termctx; ty; vars; _ } ->
+      emit (Hole (Meta.name meta, PHole (Instant instant, vars, termctx, ty)))
 
 let to_string : Command.t -> string = function
   | Axiom _ -> "axiom"

lib/parser/unparse.ml

@@ -5,6 +5,7 @@ open Tbwd
 open Bwd_extra
 open Dim
 open Core
+open Origin
 open Term
 open Notation
 open Builtins
@@ -1019,7 +1020,15 @@ let () =
             `None
       | PConstant name -> utf8string (String.concat "." (Scope.name_of name))
       | PMeta v -> utf8string (Meta.name v)
-      | PHole (vars, Permute (p, ctx), ty) ->
+      | PHole (origin, vars, Permute (p, ctx), ty) ->
+          let run =
+            match origin with
+            (* If the hole comes from an earlier time, we rewind to that time before displaying, so that the correct notations and names will be in scope. *)
+            | Instant instant when origin <> Origin.current () ->
+                Origin.rewind_command_then_undo instant
+            (* Otherwise, we give up.  Normally this would only happen when it's from the current origin (e.g. being created right now in a file) anyway. *)
+            | _ -> fun f -> f () in
+          run @@ fun () ->
           let vars, names = Names.uniquify_vars vars in
           let names, ctx = unparse_ctx names `Unlocked (Bwv.permute vars p) ctx in
           let ty = unparse names ty No.Interval.entire No.Interval.entire in

test/black/hole_in_section.t

@@ -0,0 +1,40 @@
+  $ narya -fake-interact "section foo ≔ def A : Type ≔ sig () def B : A ≔ ? def C : A ≔ ? end show hole 0 show hole 1"
+   ￫ info[I0007]
+   ￮ section foo opened
+  
+   ￫ info[I0000]
+   ￮ constant A defined
+  
+   ￫ info[I0000]
+   ￮ constant B defined, containing 1 hole
+  
+   ￫ info[I3003]
+   ￮ hole ?0:
+     
+     ----------------------------------------------------------------------
+     A
+  
+   ￫ info[I0000]
+   ￮ constant C defined, containing 1 hole
+  
+   ￫ info[I3003]
+   ￮ hole ?1:
+     
+     ----------------------------------------------------------------------
+     A
+  
+   ￫ info[I0008]
+   ￮ section foo closed
+  
+   ￫ info[I3003]
+   ￮ hole ?0:
+     
+     ----------------------------------------------------------------------
+     A
+  
+   ￫ info[I3003]
+   ￮ hole ?1:
+     
+     ----------------------------------------------------------------------
+     A
+