equal
deleted
inserted
replaced
9 |
9 |
10 (* control spacing *) |
10 (* control spacing *) |
11 |
11 |
12 val _ = |
12 val _ = |
13 Theory.setup |
13 Theory.setup |
14 (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #> |
14 (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (K (K "\\noindent")) #> |
15 Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #> |
15 Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (K (K "\\smallskip")) #> |
16 Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #> |
16 Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (K (K "\\medskip")) #> |
17 Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip")); |
17 Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (K (K "\\bigskip"))); |
18 |
18 |
19 |
19 |
20 (* control style *) |
20 (* control style *) |
21 |
21 |
22 local |
22 local |