Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Code cleanup.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Achim D. Brucker 2019-07-19 23:55:15 +01:00
parent 932b19f93d
commit e450a45c71
1 changed files with 7 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
patches/thy_output.ML
View File

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