# HG changeset patch # User wenzelm # Date 1671291714 -3600 # Node ID 7530d49d928af4af218cc7ce73cd0f828476acb0 # Parent bb8692acdcf49b23575bf74a036468e635b58640 tuned whitespace; diff -r bb8692acdcf4 -r 7530d49d928a src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Sat Dec 17 16:40:24 2022 +0100 +++ b/src/Pure/PIDE/headless.scala Sat Dec 17 16:41:54 2022 +0100 @@ -602,10 +602,10 @@ } class Resources private[Headless]( - val options: Options, - session_background: Sessions.Background, - log: Logger = No_Logger) - extends isabelle.Resources(session_background.check_errors, log = log) { + val options: Options, + session_background: Sessions.Background, + log: Logger = No_Logger) + extends isabelle.Resources(session_background.check_errors, log = log) { resources => val store: Sessions.Store = Sessions.store(options)