equal
deleted
inserted
replaced
354 case _ => |
354 case _ => |
355 } |
355 } |
356 } |
356 } |
357 } |
357 } |
358 |
358 |
|
359 |
|
360 /* mode provider */ |
|
361 |
|
362 private var orig_mode_provider: ModeProvider = null |
|
363 private var pide_mode_provider: ModeProvider = null |
|
364 |
|
365 def init_mode_provider() |
|
366 { |
|
367 orig_mode_provider = ModeProvider.instance |
|
368 if (orig_mode_provider.isInstanceOf[ModeProvider]) { |
|
369 pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider) |
|
370 ModeProvider.instance = pide_mode_provider |
|
371 } |
|
372 } |
|
373 |
|
374 def exit_mode_provider() |
|
375 { |
|
376 if (ModeProvider.instance == pide_mode_provider) |
|
377 ModeProvider.instance = orig_mode_provider |
|
378 } |
|
379 |
|
380 |
|
381 /* start and stop */ |
|
382 |
359 override def start() |
383 override def start() |
360 { |
384 { |
361 /* strict initialization */ |
385 /* strict initialization */ |
362 |
386 |
363 // adhoc patch of confusing message |
387 // adhoc patch of confusing message |
380 try { |
404 try { |
381 completion_history.load() |
405 completion_history.load() |
382 spell_checker.update(options.value) |
406 spell_checker.update(options.value) |
383 |
407 |
384 SyntaxUtilities.setStyleExtender(new Syntax_Style.Extender) |
408 SyntaxUtilities.setStyleExtender(new Syntax_Style.Extender) |
385 if (ModeProvider.instance.isInstanceOf[ModeProvider]) |
409 init_mode_provider() |
386 ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) |
|
387 |
|
388 JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _) |
410 JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _) |
389 |
411 |
390 val resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value)) |
412 val resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value)) |
391 |
413 |
392 PIDE.session.stop() |
414 PIDE.session.stop() |
408 } |
430 } |
409 |
431 |
410 override def stop() |
432 override def stop() |
411 { |
433 { |
412 JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _) |
434 JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _) |
|
435 exit_mode_provider() |
413 |
436 |
414 if (startup_failure.isEmpty) { |
437 if (startup_failure.isEmpty) { |
415 options.value.save_prefs() |
438 options.value.save_prefs() |
416 completion_history.value.save() |
439 completion_history.value.save() |
417 } |
440 } |