Subject: Fragments

Keywords: ::ReferenceEnvironment
          ::clean

Title: Fix HIE/Hrank

--------------------------------------------------
Moving STMs within theories and between theories invalidates
cached hrank and HIE.

If STMS moved between theories or theories moved, then need to fix HIE:

frag_fix_hie : bool -> tok -> int
  - if first bool arg is false then fix is ghost, just returning count of things
    to fix.
  - if second bool arg is true then hrank will default to 0,0
    Source records to not maintain hrank but default to 0,0, thus should use true
    when fixing source tables. 
    otherwise hrank is set to current position 
  - tok is table.


If STMs moved within a theory then need to fix hrank:

frag_fix_hrank : tok -> unit
  - arg is table.  
  - should fix hies if needed before fixing hranks.
⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home