diff -r c255ed582095 -r a5fda30edae2 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Tue Apr 07 21:07:28 2020 +0200 +++ b/src/Pure/PIDE/resources.scala Tue Apr 07 21:49:36 2020 +0200 @@ -265,10 +265,10 @@ def dependencies( thys: List[(Document.Node.Name, Position.T)], - progress: Progress = No_Progress): Dependencies[Unit] = + progress: Progress = new Progress): Dependencies[Unit] = Dependencies.empty[Unit].require_thys((), thys, progress = progress) - def session_dependencies(info: Sessions.Info, progress: Progress = No_Progress) + def session_dependencies(info: Sessions.Info, progress: Progress = new Progress) : Dependencies[Options] = { (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) => @@ -303,7 +303,7 @@ def require_thy(adjunct: A, thy: (Document.Node.Name, Position.T), initiators: List[Document.Node.Name] = Nil, - progress: Progress = No_Progress): Dependencies[A] = + progress: Progress = new Progress): Dependencies[A] = { val (name, pos) = thy @@ -337,7 +337,7 @@ def require_thys(adjunct: A, thys: List[(Document.Node.Name, Position.T)], - progress: Progress = No_Progress, + progress: Progress = new Progress, initiators: List[Document.Node.Name] = Nil): Dependencies[A] = (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))