equal
deleted
inserted
replaced
100 |
100 |
101 |
101 |
102 /* preview */ |
102 /* preview */ |
103 |
103 |
104 context.subscriptions.push( |
104 context.subscriptions.push( |
105 commands.registerCommand("isabelle.preview", uri => preview.request_preview(uri, false)), |
105 commands.registerCommand("isabelle.preview", uri => preview.request(uri, false)), |
106 commands.registerCommand("isabelle.preview-split", uri => preview.request_preview(uri, true)), |
106 commands.registerCommand("isabelle.preview-split", uri => preview.request(uri, true)), |
107 commands.registerCommand("isabelle.preview-source", preview.show_source), |
107 commands.registerCommand("isabelle.preview-source", preview.source), |
108 commands.registerCommand("isabelle.preview-update", preview.update_preview)) |
108 commands.registerCommand("isabelle.preview-update", preview.update)) |
109 |
109 |
110 language_client.onReady().then(() => preview.init(context, language_client)) |
110 language_client.onReady().then(() => preview.init(context, language_client)) |
111 |
111 |
112 |
112 |
113 /* start server */ |
113 /* start server */ |