*** Failed to relativize href location

[Makarius]

On 22/04/2026 11:57, Makarius wrote:
> On 22/04/2026 11:37, Tobias Nipkow wrote:
>> ...
>> Presenting theory "Dyck_Language.Dyck_Language"
>> Presenting theory "Pure"
>> *** Failed to relativize href location "/Users/nipkow/.isabelle/ 
>> browser_info/ HOL/HOL/ISABELLE_HOME/src/Provers/classical.ML.html" with wrt. 
>> base "/Users/ nipkow/.isabelle/browser_info/AFP/Context_Free_Grammar"
>>
>> AFP: parent: 16494:e2ca723aa27e tip
>> Isabelle: parent: 84518:f09a1737d3c0 tip
>>
>> What am I doing wrong :)
> 
> I've got something wrong in b8b99a2c5991 with the semantics of 
> File.relative_path vs. _.relativize(_) --- and need to investigate this further.

I would say it should work again with the subsequent change, but your "..." 
above don't say in which situation the problem actually occurred, so I could 
not reproduce it.

changeset:   84520:c50c2ebb9f7c
user:        wenzelm
date:        Wed Apr 22 12:45:30 2026 +0200
files:       src/Pure/General/file.scala src/Pure/General/html.scala
description:
more permissive operation, for relative locations outside the base (amending 
b8b99a2c5991, see also 02588021b581);


	Makarius