File tree 2 files changed +3
-3
lines changed
2 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -119,7 +119,7 @@ fun export_phases thy name =
119
119
val path = Path.binding (
120
120
Path.append directory filename ,
121
121
Position.none ) ;
122
- val thy' = thy | > Generated_Files.add_files ( path , content ) ;
122
+ val thy' = thy | > Generated_Files.add_files ( path , ( Bytes.string content ) ) ;
123
123
124
124
val _ = Export.export thy' path [ YXML.parse cleaned ] ;
125
125
@@ -131,7 +131,7 @@ fun export_phases thy name =
131
131
val _ =
132
132
Outer_Syntax.command \<^command_keyword >\<open>export_phases\<close>
133
133
"export information about encoded optimizations"
134
- ( Parse.text >>
134
+ ( Parse.path >>
135
135
( fn name = > Toplevel.theory ( fn state = > export_phases state name )))
136
136
\<close>
137
137
Original file line number Diff line number Diff line change @@ -25,7 +25,7 @@ fun wrapped_command (command: string) (name: string option) =
25
25
in
26
26
Document_Output.document_output
27
27
{markdown = false,
28
- markup = fn _ => Latex.enclose_text "%\n" "\n" (Latex.string latex)}
28
+ markup = fn _ => XML.enclose "%\n" "\n" (Latex.string latex)}
29
29
(*(Pure_Syn.document_command {markdown = false} (NONE, doc))*)
30
30
end
31
31
You can’t perform that action at this time.
0 commit comments