From e450a45c7196fa357b25da57df5491bb5b432c32 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Fri, 19 Jul 2019 23:55:15 +0100
Subject: [PATCH] Code cleanup.

---
 patches/thy_output.ML | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/patches/thy_output.ML b/patches/thy_output.ML
index fac1024..b0a8212 100644
--- a/patches/thy_output.ML
+++ b/patches/thy_output.ML
@@ -353,19 +353,16 @@ val ignore =
     (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
     >> pair (d - 1));
 
-
 val locale =
   Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
     Parse.!!!
       (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
 
-
 (*
 val meta_args_parser_hook =  Synchronized.var "meta args parser hook" 
                              ((fn thy => fn s => ("",s)): theory -> string parser);
 *)
-val meta_args_parser_hook =  Unsynchronized.ref 
-                             ((fn _ => fn s => ("",s)): theory -> string parser);
+val meta_args_parser_hook =  Unsynchronized.ref ((fn _ => fn s => ("",s)): theory -> string parser);
 
 in
 
@@ -381,7 +378,6 @@ fun present_thy options thy (segments: segment list) =
     val ignored = Scan.state --| ignore
       >> (fn d => (NONE, (Ignore_Token, ("", d))));
 
-
     fun markup pred mk flag = Scan.peek (fn d =>
       Document_Source.improper 
       |-- Parse.position (Scan.one (fn tok => Token.is_command tok andalso 
@@ -476,9 +472,12 @@ fun present_thy options thy (segments: segment list) =
     else error "Messed-up outer syntax for presentation"
   end;
 
-fun set_meta_args_parser f = let val _ = writeln "Meta-args parser set to new value" 
-                             in  ( meta_args_parser_hook := f) end
-
+  fun set_meta_args_parser f = 
+    let
+      val _ = writeln "Meta-args parser set to new value"                          
+    in  
+      (meta_args_parser_hook := f)
+    end
 
 end;