tuned headers;
authorwenzelm
Sun, 12 Jan 2025 13:27:47 +0100
changeset 81776 c6d8db03dfdc
parent 81775 1a02f32f7d20
child 81777 9346640e6cda
tuned headers;
src/Pure/GUI/font_metric.scala
src/Pure/PIDE/markup_kind.ML
--- a/src/Pure/GUI/font_metric.scala	Sun Jan 12 13:27:11 2025 +0100
+++ b/src/Pure/GUI/font_metric.scala	Sun Jan 12 13:27:47 2025 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/GUI/gui.scala
+/*  Title:      Pure/GUI/font_metric.scala
     Author:     Makarius
 
 Precise metric for smooth font rendering, notably for pretty-printing.
--- a/src/Pure/PIDE/markup_kind.ML	Sun Jan 12 13:27:11 2025 +0100
+++ b/src/Pure/PIDE/markup_kind.ML	Sun Jan 12 13:27:47 2025 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/markup_kind.ML
+(*  Title:      Pure/PIDE/markup_kind.ML
     Author:     Makarius
 
 Formally defined kind for Markup.notation and Markup.expression.