Email Gateway (Jan 22 2024 at 12:32): Email Gateway (Jan 22 2024 at 12:32):From: Tobias Nipkow <nipkow@in.tum.de>
I am on 57ceacd4a17b and in src/HOL/Library. isabelle jedit Tree_Real.thy
tells me
Bad theory import "HOL-Library.Tree"
If I click on the theory name, it loads. With Isabelle23 the theory was loaded
automatically, no Bad import. This seems a fairly recent change. Is it itended?
Tobias
Email Gateway (Jan 22 2024 at 19:53):From: Makarius <makarius@sketis.net>
Thanks for the problem report on the isabelle-dev repository (the proper
channel is the isabelle-dev mailing list).
Bisection over the history points to the following recent change:
changeset: 79510:d8330439823a
user: wenzelm
date: Sun Jan 21 14:05:14 2024 +0100
summary: clarified signature: explicit type isabelle.Url to avoid oddities
of java.net.URL (e.g. its "equals" method);
You can continue on the spot with its parent e82448aacf48, while I am
investigating the situation.
Makarius
Email Gateway (Jan 22 2024 at 21:48):From: Makarius <makarius@sketis.net>
Here is the result of the investigation:
changeset: 79514:9204c034a5bf
tag: tip
user: wenzelm
date: Mon Jan 22 22:18:20 2024 +0100
files: src/Pure/General/url.scala
description:
recover Url.is_wellformed from before d8330439823a, e.g. relevant for
JEdit_Resources.read_file_content (the URI alone does not necessarily have a
protocol prefix, so plain file-path would be treated as URL);
Makarius
Last updated: Jan 04 2025 at 20:18 UTC