The "Outline" window allows to click on commands to select according spans in the source text. This should be restricted to the "proper_range" (according to the Isabelle/Scala method Command.proper_range) to avoid including the trailing whitespace. (It is in fact a recurrent fine-point of all prover interfaces and IDEs in the last 15 years.)
The "Outline" window allows to click on commands to select according spans in the source text. This should be restricted to the "proper_range" (according to the Isabelle/Scala method Command.proper_range) to avoid including the trailing whitespace. (It is in fact a recurrent fine-point of all prover interfaces and IDEs in the last 15 years.)